ι : Sort ?u.273037
f : ι → ℝ≥0
α : Sort u_1
⊢ (⨅ (i : α), ↑0) = ↑0
ι : Sort ?u.273037
f : ι → ℝ≥0
α : Sort u_1
⊢ (⨅ (x : α), 0) = 0
rw [← NNReal.coe_eq, coe_iInf]
no goals
ι : Sort ?u.273037
f : ι → ℝ≥0
α : Sort u_1
⊢ (⨅ (i : α), ↑0) = ↑0
exact Real.ciInf_const_zero