ι : Sort u_1
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))
ι : Sort u_1
s : ι → ℝ≥0
⊢ ↑(⨅ (i : ι), s i) = ⨅ (i : ι), ↑(s i)
rw [iInf, iInf, coe_sInf, ← Set.range_comp]
no goals
ι : Sort u_1
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i => s i)) = sInf (Set.range fun i => ↑(s i))
rfl