Theorems · Theorem · order theory
IsCompl.dual
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α] {x y : α},
IsCompl x y → IsCompl (OrderDual.toDual x) (OrderDual.toDual y)- Defined in
- Mathlib.Order.Disjoint
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses Quot.sound
- Assumes
- PartialOrderBoundedOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Equivstatement · cited by 8,337
- PartialOrderstatement and proof · cited by 6,410
- OrderDualstatement · cited by 927
- OrderDual.toDualstatement · cited by 481
- IsComplstatement and proof · cited by 351
- BoundedOrderstatement and proof · cited by 270
- IsCompl.disjointproof · cited by 42
- IsCompl.codisjointproof · cited by 32
Cited by6
Results whose statement or proof uses this declaration.
- IsCompl.le_sup_right_iff_inf_left_leproof · cited by 2
- IsCompl.left_le_iffproof · cited by 1
- eq_bot_of_isCompl_topproof · cited by 0
- eq_bot_of_top_isComplproof · cited by 0
- isCompl_ofDual_iffproof · cited by 0
- isCompl_toDual_iffproof · cited by 0