Theorems · Theorem · general topology
Filter.le_generate_iff
∀ {α : Type u} {s : Set (Set α)} {f : Filter α}, f ≤ Filter.generate s ↔ s ⊆ f.sets- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
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
- Filter.inter_memproof · cited by 153
- Filter.univ_memproof · cited by 96
- Filter.setsstatement and proof · cited by 56
- Filter.generatestatement and proof · cited by 30
- Filter.GenerateSetsproof · cited by 3
- Filter.GenerateSets.recOnproof · cited by 1
Cited by8
Results whose statement or proof uses this declaration.
- Filter.giGenerateproof · cited by 6
- FilterBasis.generateproof · cited by 4
- UniformFun.gcproof · cited by 2
- Filter.atTop_eq_generate_of_forall_exists_leproof · cited by 1
- Filter.atBot_eq_generate_of_forall_exists_leproof · cited by 1
- Filter.map_generate_le_generate_preimage_preimageproof · cited by 0
- Filter.generate_image_preimage_le_comapproof · cited by 0
- Filter.generate_singletonproof · cited by 0