Theorems · Theorem · general topology
Filter.inf_principal
∀ {α : Type u} {s t : Set α}, Filter.principal s ⊓ Filter.principal t = Filter.principal (s ∩ t)- Defined in
- Mathlib.Order.Filter.Basic
- Cited by
- 29 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Quot.sound
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 · cited by 8,121
- le_antisymmproof · cited by 2,068
- Filter.principalstatement · cited by 740
- Set.Subset.rflproof · cited by 255
Cited by29
Results whose statement or proof uses this declaration.
- TopologicalSpace.nhds_generateFromproof · cited by 15
- Filter.prod_principal_principalproof · cited by 9
- nhdsWithin_interproof · cited by 6
- hasDerivWithinAt_iff_tendsto_slopeproof · cited by 6
- nhds_eq_iInf_abs_subproof · cited by 5
- IsLindelof.inter_rightproof · cited by 4
- accPt_principal_iff_clusterPtproof · cited by 4
- Preperfect.perfect_closureproof · cited by 3
- Filter.iInf_principal_finsetproof · cited by 3
- nhdsWithin_inter'proof · cited by 3
- Filter.mem_inf_principal'proof · cited by 2
- Filter.lift'_iInf_of_map_univproof · cited by 2