Theorems · Theorem · order theory
iSupIndep.disjoint_biSup_biSup
∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {ι : Type u_3} [IsModularLattice α] {f : ι → α}
{s t : Set ι}, iSupIndep f → Disjoint s t → Disjoint (⨆ i ∈ s, f i) (⨆ i ∈ t, f i)- Defined in
- Mathlib.Order.CompactlyGenerated.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- iSupstatement · cited by 2,415
- Disjointstatement and proof · cited by 2,201
- Set.Finiteproof · cited by 1,814
- CompleteLatticestatement and proof · cited by 1,048
- iSupIndepstatement and proof · cited by 100
- IsModularLatticestatement and proof · cited by 86
- IsCompactlyGeneratedstatement and proof · cited by 37
- Set.disjoint_of_subset_leftproof · cited by 17
- disjoint_biSup_of_finite_disjoint_biSupproof · cited by 1
- iSupIndep.disjoint_biSup_biSup'proof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- LieAlgebra.Basis.iSupIndep_rootSpaceproof · cited by 3