Theorems · Theorem · general topology
Filter.HasBasis.disjoint_iff_left
∀ {α : Type u_1} {ι : Sort u_4} {l l' : Filter α} {p : ι → Prop} {s : ι → Set α},
l.HasBasis p s → (Disjoint l l' ↔ ∃ i, p i ∧ (s i)ᶜ ∈ l')- Defined in
- Mathlib.Order.Filter.Bases.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, 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
- Compl.complstatement · cited by 2,925
- Disjointstatement and proof · cited by 2,201
- Filter.HasBasisstatement and proof · cited by 604
- Filter.basis_setsproof · cited by 105
- Filter.HasBasis.disjoint_iffproof · cited by 13
- Filter.hasBasis_principalproof · cited by 8
Cited by11
Results whose statement or proof uses this declaration.
- IsCompact.disjoint_nhdsSet_leftproof · cited by 6
- isCompact_of_finite_subcoverproof · cited by 5
- isLindelof_of_countable_subcoverproof · cited by 4
- Filter.HasBasis.disjoint_iff_rightproof · cited by 3
- IsLindelof.compl_mem_sets_of_nhdsWithinproof · cited by 2
- SeminormedGroup.disjoint_nhdsproof · cited by 1
- Filter.HasBasis.disjoint_cobounded_iffproof · cited by 1
- SeminormedAddGroup.disjoint_nhdsproof · cited by 1
- IsLindelof.disjoint_nhdsSet_leftproof · cited by 1
- Metric.exists_isBounded_image_of_tendstoproof · cited by 1
- Filter.disjoint_cocompact_leftproof · cited by 0