Theorems · Theorem · order theory
IsCompl.disjoint
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Disjoint x yIf x and y are to be complementary in an order, they should be disjoint.
- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 42 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- PartialOrderBoundedOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Disjointstatement · cited by 2,201
- IsComplstatement and proof · cited by 351
- BoundedOrderstatement and proof · cited by 270
Cited by42
Results whose statement or proof uses this declaration.
- IsCompl.symmproof · cited by 80
- IsCompl.compl_eqproof · cited by 16
- IsCompl.inf_eq_botproof · cited by 11
- isCompl_iffproof · cited by 8
- IsCompl.dualproof · cited by 6
- IsCompl.eq_complproof · cited by 4
- linearIndependent_sumproof · cited by 3
- LinearMap.iSup_range_single_eq_iInf_ker_projproof · cited by 2
- LinearMap.BilinForm.isCompl_orthogonal_iff_disjointproof · cited by 2
- Submodule.finrank_add_eq_of_isComplproof · cited by 2
- IsCompl.mapproof · cited by 2
- IsCompl.ofDualproof · cited by 2