Theorems · Theorem · general topology
Filter.mp_mem
∀ {α : Type u_1} {f : Filter α} {s t : Set α}, s ∈ f → {x | x ∈ s → x ∈ t} ∈ f → t ∈ f- Defined in
- Mathlib.Order.Filter.Defs
- Cited by
- 1,537 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 21 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.ofPredstatement and proof · cited by 6,101
- Filter.mem_of_supersetproof · cited by 308
- Filter.inter_memproof · cited by 153
Cited by1,537
Results whose statement or proof uses this declaration.
- Filter.Eventually.mpproof · cited by 78
- meromorphicOrderAt_eq_int_iffproof · cited by 31
- MeasureTheory.Measure.rnDeriv_lt_topproof · cited by 21
- MeasureTheory.lintegral_prodproof · cited by 20
- meromorphicOrderAt_eq_top_iffproof · cited by 20
- ContMDiffWithinAt.compproof · cited by 18
- Filter.tendsto_atTop_mono'proof · cited by 17
- MeasureTheory.integral_mono_aeproof · cited by 15
- meromorphicOrderAt_congrproof · cited by 15
- Asymptotics.IsBigOWith.transproof · cited by 13
- MeromorphicAt.congrproof · cited by 12
- Filter.Tendsto.atTop_mul_atTop₀proof · cited by 12
Showing the 200 most cited of 1,537.