Theorems · Theorem · order theory
le_ciSup
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f : ι → α},
BddAbove (Set.range f) → ∀ (c : ι), f c ≤ iSup fThe indexed supremum of a function is bounded below by the value taken at one point
- Cited by
- 57 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- ConditionallyCompleteLattice
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.
- Set.rangestatement and proof · cited by 4,705
- iSupstatement · cited by 2,415
- BddAbovestatement and proof · cited by 620
- ConditionallyCompleteLatticestatement and proof · cited by 364
- Set.mem_range_selfproof · cited by 328
- le_csSupproof · cited by 66
Cited by57
Results whose statement or proof uses this declaration.
- ciInf_leproof · cited by 25
- Module.Basis.mk_eq_rank''proof · cited by 23
- le_ciSup_of_leproof · cited by 22
- Ordinal.le_iSupproof · cited by 19
- LinearIndependent.cardinal_lift_le_rankproof · cited by 16
- lift_rank_range_leproof · cited by 7
- Cardinal.preBeth_limitproof · cited by 5
- MvPowerSeries.le_gaussNormproof · cited by 5
- Polynomial.gaussNorm_coe_powerSeriesproof · cited by 4
- Ordinal.lift_cof_iSup_add_oneproof · cited by 4
- Cardinal.le_powerltproof · cited by 4
- ciSup_subtypeproof · cited by 4