Theorems · Theorem · order theory
IsCompl.sup_eq_top
∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → x ⊔ y = ⊤- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
- Assumes
- LatticeBoundedOrder
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.
- Top.topstatement · cited by 9,680
- Latticestatement and proof · cited by 916
- IsComplstatement and proof · cited by 351
- BoundedOrderstatement and proof · cited by 270
- IsCompl.codisjointproof · cited by 32
- Codisjoint.eq_topproof · cited by 22
Cited by20
Results whose statement or proof uses this declaration.
- eq_top_of_isCompl_botproof · cited by 4
- Set.range_inl_union_range_inrproof · cited by 3
- Set.insert_none_range_someproof · cited by 3
- IsCompl.prod_mul_prodproof · cited by 2
- IsCompl.sum_add_sumproof · cited by 2
- IsCompl.sup_infproof · cited by 2
- LinearMap.IsSymm.nondegenerate_restrict_of_isCompl_kerproof · cited by 1
- RootPairing.orthogonal_rootSpan_eqproof · cited by 1
- LinearMap.projectionOnto_of_projproof · cited by 1
- Subgroup.IsComplement'.sup_eq_topproof · cited by 1
- Module.Dual.eq_of_ker_eq_of_apply_eqproof · cited by 1