Theorems · Theorem · order theory
le_sup_of_le_right
∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ b → c ≤ a ⊔ b- Defined in
- Mathlib.Order.Lattice
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 4 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_transproof · cited by 985
- SemilatticeSupstatement and proof · cited by 785
- le_sup_rightproof · cited by 242
Cited by17
Results whose statement or proof uses this declaration.
- sup_le_supproof · cited by 48
- le_max_of_le_rightproof · cited by 30
- IsLUB.unionproof · cited by 5
- OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_ltproof · cited by 4
- iSup_orproof · cited by 3
- symmDiff_sup_infproof · cited by 2
- Finset.le_prod_max_oneproof · cited by 2
- Set.bounded_le_inter_not_leproof · cited by 2
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_leftproof · cited by 2
- SupPrime.le_supproof · cited by 1
- LieSubmodule.lcs_le_lcs_of_is_nilpotent_span_sup_eq_topproof · cited by 1
- LieAlgebra.lieIdeal_eq_inf_cartan_sup_biSup_inf_rootSpaceproof · cited by 1