OAI/Geometry/Cannon/Modulus/Ambient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonCarrierCharging.radial_level_preimage line 17
  2. theorem OAI.CannonCarrierCharging.radial_continua_carrier_crossing line 27
  3. lemma OAI.CannonCarrierCharging.circle_carriers_preconnected line 48
  4. lemma OAI.CannonCarrierCharging.spherical_radial_level_preimage line 65
  5. theorem OAI.CannonCarrierCharging.spherical_continua_carrier_crossing line 100
  6. lemma OAI.CannonCarrierCharging.spherical_circle_carriers_preconnected line 126
  7. theorem OAI.CannonRelease.boundary_annular_circle_carriers line 148
  8. theorem OAI.CannonRadialEnergy.local_radial_cell_energy_budget line 207
  9. theorem OAI.CannonCarrierCharging.metric_carrier_modulus_bound line 245
  10. abbrev OAI.CannonRoundRadial.Ambient line 309
  11. abbrev OAI.CannonRoundRadial.Round line 310
  12. theorem OAI.CannonRoundRadial.metric_sphere_preconnected line 312
  13. theorem OAI.CannonRoundRadial.metric_circle_carriers_preconnected line 403