OAI/Geometry/RCD/Metric/FiniteSeparationCode.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite measurable codes exhaust the off-diagonal

A countable separating family can be truncated without losing more than an arbitrarily small part of a finite measure on pairs.

  1. def OAI.RegularPointCoordinates.finiteSeparationCode line 17
  2. theorem OAI.RegularPointCoordinates.measurable_finiteSeparationCode line 21
  3. def OAI.RegularPointCoordinates.codeSeparatedPairs line 28
  4. theorem OAI.RegularPointCoordinates.measurableSet_codeSeparatedPairs line 31
  5. theorem OAI.RegularPointCoordinates.monotone_codeSeparatedPairs line 37
  6. theorem OAI.RegularPointCoordinates.iUnion_codeSeparatedPairs line 46
  7. theorem OAI.RegularPointCoordinates.tendsto_codeSeparatedPairs_measure line 67
  8. theorem OAI.RegularPointCoordinates.exists_finite_separation_code line 75