Theorems · Theorem · general topology
Filter.sets_of_superset
∀ {α : Type u_1} (self : Filter α) {x y : Set α}, x ∈ self.sets → x ⊆ y → y ∈ self.setsIf a set belongs to a filter, then its superset belongs to the filter as well.
- Defined in
- Mathlib.Order.Filter.Defs
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 6 from the axioms · 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 · cited by 53,352
- Filterstatement and proof · cited by 8,121
- Filter.setsstatement · cited by 56
Cited by14
Results whose statement or proof uses this declaration.
- Filter.mem_of_supersetproof · cited by 308
- Filter.image_mem_mapproof · cited by 39
- isLindelof_of_countable_subcoverproof · cited by 4
- Asymptotics.SuperpolynomialDecay.param_mulproof · cited by 3
- limsSup_nhdsproof · cited by 2
- uniformity_eq_uniformity_interiorproof · cited by 1
- Filter.atTop_eq_generate_of_forall_exists_leproof · cited by 1
- Filter.pure_seq_eq_mapproof · cited by 1
- LaurentSeries.Cauchy.coeff_eventually_equalproof · cited by 1
- LaurentSeries.Cauchy.exists_lb_coeff_neproof · cited by 1
- Filter.seq_pureproof · cited by 1
- Filter.atBot_eq_generate_of_forall_exists_leproof · cited by 1