OAI/Geometry/Kahler/BaseCompositionJets.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.PinchedHartogs.BaseConstruction.analytic_real_jet_normline 20 - lemma
OAI.PinchedHartogs.BaseConstruction.small_power_boundline 27 - lemma
OAI.PinchedHartogs.BaseConstruction.norm_composition_jet_linearline 39 - lemma
OAI.PinchedHartogs.BaseConstruction.smooth_jet_bound_compactline 60