OAI/Geometry/TamingCompatibility/Hodge/HodgeSeparatingMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.separating_current_mass_and_cross line 26
2. theorem OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.exists_counterexample_mass_cross line 55
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.finite_common_parametrix_partition line 86