English
For a set s of ENNReal numbers, the NNReal of the infimum of s equals the infimum of the NNReal-images of s, provided none of the elements is ∞: (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s).
Русский
Для множества s ENNReal верна эквивалентность: (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s), при условии, что все элементы не равны ∞.
LaTeX
$$$ (\mathrm{sInf}\ s).toNNReal = \mathrm{sInf}\ (\mathrm{ENNReal.toNNReal} '' s) $$$
Lean4
theorem toNNReal_sInf (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) : (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s) :=
by
have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
simpa only [← sInf_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iInf hf)
