OAI/Geometry/RCD/Metric/LocalDensityGluing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Gluing almost-everywhere local constants on a Euclidean ball

  1. theorem OAI.RegularPointCoordinates.ae_constants_eq_on_open_overlap line 13
  2. theorem OAI.RegularPointCoordinates.ae_constant_on_ball_of_locally_constant line 26