Theorems · Theorem · order theory
sup_le_sup_right
∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, a ≤ b → ∀ (c : α), a ⊔ c ≤ b ⊔ c- Defined in
- Mathlib.Order.Lattice
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- SemilatticeSup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- le_rflproof · cited by 1,558
- SemilatticeSupstatement and proof · cited by 785
- sup_le_supproof · cited by 48
Cited by14
Results whose statement or proof uses this declaration.
- sup_sdiff_eq_supproof · cited by 3
- strictMono_inf_prod_supproof · cited by 2
- Codisjoint.codisjoint_inf_right_of_codisjoint_inf_leftproof · cited by 2
- Codisjoint.le_of_disjointproof · cited by 2
- Finite.ciSup_supproof · cited by 1
- sInf_sup_le_iInf_supproof · cited by 1
- oneLePart_monoproof · cited by 1
- leOnePart_antiproof · cited by 1
- posPart_monoproof · cited by 1
- negPart_antiproof · cited by 1
- sup_lt_sup_of_lt_of_inf_le_infproof · cited by 1
- max_le_max_rightproof · cited by 1