OAI/Analysis/RieszRectifiability/Nets/SeparatedSupportNets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Maximal separated extensions give covering nets. Positive separation also gives discreteness, countability in separable spaces, and finiteness on compact sets.

  1. theorem OAI.RieszRectifiability.exists_separated_cover_extension line 17
  2. theorem OAI.RieszRectifiability.separated_set_countable line 46
  3. theorem OAI.RieszRectifiability.separated_set_discrete line 56
  4. theorem OAI.RieszRectifiability.separated_set_finite_inter_compact line 72