Theorems · Theorem · order theory
le_sup_of_le_left
∀ {α : Type u} [inst : SemilatticeSup α] {a b c : α}, c ≤ a → c ≤ a ⊔ b- Defined in
- Mathlib.Order.Lattice
- Cited by
- 26 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_leftproof · cited by 265
Cited by26
Results whose statement or proof uses this declaration.
- sup_le_supproof · cited by 48
- le_max_of_le_leftproof · cited by 31
- IsLUB.unionproof · cited by 5
- cauchySeq_finset_iff_sum_vanishingproof · cited by 5
- iSup_orproof · cited by 3
- cauchySeq_finset_iff_prod_vanishingproof · cited by 3
- symmDiff_sup_infproof · cited by 2
- Set.bounded_le_inter_not_leproof · cited by 2
- Coheyting.boundary_le_boundary_sup_sup_boundary_inf_leftproof · cited by 2
- Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRingproof · cited by 2
- LieAlgebra.IsKilling.mem_rootSet_invtSubmoduleToLieIdealproof · cited by 2
- SupPrime.le_supproof · cited by 1