OAI/Geometry/CAT0Fillings/Calculus/ClosedChain.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CAT0Fillings.ChartGeometry.atlas_preservingline 17 - def
OAI.CAT0Fillings.ChartGeometry.composeValueline 20 - lemma
OAI.CAT0Fillings.ChartGeometry.composeValue_aeline 24 - lemma
OAI.CAT0Fillings.ChartGeometry.continuous_composeValueline 38 - lemma
OAI.CAT0Fillings.ChartGeometry.composeValue_valueline 42 - lemma
OAI.CAT0Fillings.ChartGeometry.closed_chainline 52