x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ sSup (Set.range fun i => f i) = 0
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ (⨆ (i : α), f i) = 0
dsimp [iSup]
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ (Set.range fun i => f i) = ∅
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ sSup (Set.range fun i => f i) = 0
convert Real.sSup_empty
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ IsEmpty α
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ (Set.range fun i => f i) = ∅
rw [Set.range_eq_empty_iff]
no goals
case h.e'_2.h.e'_3
x y : ℝ
α : Sort u_1
inst✝ : IsEmpty α
f : α → ℝ
⊢ IsEmpty α
infer_instance