Theorems · Theorem · general topology
Filter.le_countableGenerate_iff_of_countableInterFilter
∀ {α : Type u_2} {g : Set (Set α)} {f : Filter α} [CountableInterFilter f], f ≤ Filter.countableGenerate g ↔ g ⊆ f.sets- Defined in
- Mathlib.Order.Filter.CountableInter
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CountableInterFilter
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Set.Countableproof · cited by 545
- Filter.mem_of_supersetproof · cited by 308
- Filter.univ_memproof · cited by 96
- CountableInterFilterstatement and proof · cited by 78
- subset_transproof · cited by 63
- Filter.setsstatement and proof · cited by 56
- countable_sInter_memproof · cited by 6
- Filter.CountableGenerateSetsproof · cited by 3
- Filter.countableGeneratestatement and proof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- tendsto_residual_of_isOpenMapproof · cited by 3
- Filter.countableGenerate_isGreatestproof · cited by 0