OAI/Analysis/SeparableQuotients/Positive/SeparatedFamilies.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SeparableQuotient.Positive.Family.ContinuumIndex line 12
2. abbrev OAI.SeparableQuotient.Positive.Family.continuumMeasurableSpace line 13
3. abbrev OAI.SeparableQuotient.Positive.Family.ContinuumAdditive line 14
4. lemma OAI.SeparableQuotient.Positive.Family.exists_separated_cover line 29
5. theorem OAI.SeparableQuotient.Positive.Family.exists_large_separated_of_density line 55
6. lemma OAI.SeparableQuotient.Positive.Family.closure_rat_span_eq_real line 99
7. lemma OAI.SeparableQuotient.Positive.Family.card_rat_span_le line 120
8. lemma OAI.SeparableQuotient.Positive.Family.large_separated_away_small_closure line 142
9. lemma OAI.SeparableQuotient.Positive.Family.exists_unit_dual_annihilating line 170