Theorems · Theorem · general topology
Filter.mem_of_superset
∀ {α : Type u_1} {f : Filter α} {x y : Set α}, x ∈ f → x ⊆ y → y ∈ f- Defined in
- Mathlib.Order.Filter.Defs
- Cited by
- 308 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 13 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.sets_of_supersetproof · cited by 14
Cited by308
Results whose statement or proof uses this declaration.
- Filter.univ_mem'proof · cited by 1,672
- Filter.mp_memproof · cited by 1,537
- Filter.le_principal_iffproof · cited by 87
- Filter.eventually_of_memproof · cited by 43
- Filter.Ioi_mem_atTopproof · cited by 36
- Filter.HasBasis.ge_iffproof · cited by 28
- IsCompact.prodproof · cited by 26
- ContinuousOn.aestronglyMeasurableproof · cited by 21
- Metric.closedBall_mem_nhdsproof · cited by 20
- Icc_mem_nhdsproof · cited by 20
- Filter.map_le_iff_le_comapproof · cited by 19
- Filter.empty_mem_iff_botproof · cited by 18
Showing the 200 most cited of 308.