Theorems · Theorem · order theory
IsCompl.codisjoint
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → Codisjoint x yIf x and y are to be complementary in an order, they should be codisjoint.
- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 32 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
- IsComplstatement and proof · cited by 351
- BoundedOrderstatement and proof · cited by 270
- Codisjointstatement · cited by 197
Cited by32
Results whose statement or proof uses this declaration.
- IsCompl.symmproof · cited by 80
- IsCompl.sup_eq_topproof · cited by 20
- IsCompl.compl_eqproof · cited by 16
- isCompl_iffproof · cited by 8
- IsCompl.dualproof · cited by 6
- IsCompl.eq_complproof · cited by 4
- LinearMap.iSup_range_single_eq_iInf_ker_projproof · cited by 2
- ComplementedLattice.isStronglyAtomicproof · cited by 2
- Submodule.finrank_add_eq_of_isComplproof · cited by 2
- IsCompl.mapproof · cited by 2
- IsCompl.ofDualproof · cited by 2
- LinearMap.iSup_range_singleproof · cited by 1