ι : Sort ?u.272153
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0
ι : Sort ?u.272153
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0
rw [← bddAbove_coe] at hs
ι : Sort ?u.272153
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0
ι : Sort ?u.272153
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup s = 0
rw [← NNReal.coe_eq, coe_sSup, NNReal.coe_zero]
no goals
ι : Sort ?u.272153
f : ι → ℝ≥0
s : Set ℝ≥0
hs : ¬BddAbove (toReal '' s)
⊢ sSup (toReal '' s) = 0
exact sSup_of_not_bddAbove hs