OAI/Geometry/Cannon/Energy/SquareMap.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.CannonCharts.rectangle_modulus_localizationline 28 - def
OAI.CannonCharts.squareMapline 62 - lemma
OAI.CannonCharts.continuous_squareMapline 64 - lemma
OAI.CannonCharts.squareMap_injectiveline 68 - lemma
OAI.CannonCharts.squareMap_embeddingline 80 - lemma
OAI.CannonCharts.squareMap_in_boxline 83 - theorem
OAI.CannonCharts.lift_strip_crossingline 89 - theorem
OAI.CannonCharts.stripFamily_eq_imageline 113