OAI/Geometry/IsometricImmersion/Caps/UpperCapMetricJets.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.SmoothLocal.Flow.Reflection.UpperCapMetricJetBudgetline 13 - def
OAI.SmoothLocal.Flow.Reflection.LocalUpperCapMetricJetsline 15 - def
OAI.SmoothLocal.Flow.Reflection.reflectedUpperRectangleline 20 - theorem
OAI.SmoothLocal.Flow.Reflection.reflectedUpperRectangle_lowerline 34 - theorem
OAI.SmoothLocal.Flow.Reflection.reflectedUpperRectangle_imageline 39 - def
OAI.SmoothLocal.Flow.Reflection.reflectedUpperBudgetline 44 - theorem
OAI.SmoothLocal.Flow.Reflection.reflectedMetric_localCapJetsline 47 - theorem
OAI.SmoothLocal.Flow.Reflection.conjugateFlow_twiceline 57