Theorems · Theorem · order theory
isLUB_ciSup
∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
BddAbove (Set.range f) → IsLUB (Set.range f) (⨆ i, f i)- Cited by
- 10 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- IsLUBstatement · cited by 280
- Set.range_nonemptyproof · cited by 84
- isLUB_csSupproof · cited by 34
Cited by10
Results whose statement or proof uses this declaration.
- Measurable.iSupproof · cited by 14
- ciSup_le_iffproof · cited by 6
- lp.isLUB_normproof · cited by 6
- Ordinal.isNormal_derivFamilyproof · cited by 5
- memℓp_gen'proof · cited by 4
- NNReal.Lp_add_le_tsumproof · cited by 4
- NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsumproof · cited by 4
- Real.isLUB_of_tendsto_monotone_bddAboveproof · cited by 0
- Orthonormal.inner_products_summableproof · cited by 0