Theorems · Theorem · order theory
disjoint_iff
∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b ↔ a ⊓ b = ⊥- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- SemilatticeInfOrderBot
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Bot.botstatement · cited by 4,720
- Disjointstatement · cited by 2,201
- OrderBotstatement and proof · cited by 1,055
- SemilatticeInfstatement and proof · cited by 634
- le_bot_iffproof · cited by 116
- disjoint_iff_inf_leproof · cited by 64
Cited by76
Results whose statement or proof uses this declaration.
- Set.disjoint_iff_inter_eq_emptyproof · cited by 49
- Filter.disjoint_principal_rightproof · cited by 10
- Module.End.disjoint_genEigenspaceproof · cited by 7
- IsCompl.of_eqproof · cited by 7
- Submodule.supIndep_torsionBySet_idealproof · cited by 4
- Module.End.independent_genEigenspaceproof · cited by 4
- Finset.disjoint_iff_inter_eq_emptyproof · cited by 4
- Subgroup.disjoint_of_coprime_natCardproof · cited by 3
- BoxIntegral.Prepartition.eventually_splitMany_inf_eq_filterproof · cited by 3
- MonoidHom.ker_transferSylow_isComplement'proof · cited by 3
- LieSubmodule.disjoint_toSubmoduleproof · cited by 3
- LieAlgebra.InvariantForm.orthogonal_disjointproof · cited by 3