coe_iInf — Mathlib

English

For a nonempty index set ι and f: ι → ℝ≥0, the ENNReal of the infimum equals the infimum over i of ENNReal.ofNNReal(f(i)); i.e. ↑(iInf f) = ⨅ a, ↑(f a).

Русский

Для непустого множества индексов ι и f: ι → ℝ≥0, ENNReal.ofNNReal(Inf f) равно Inf образов f в ENNReal: ↑(iInf f) = ⨅ a, ↑(f a).

LaTeX

$$$$\\uparrow(\\mathrm{iInf}\\ f) = \\bigwedge_{a} \\uparrow(f(a))$$$$

Lean4

@[norm_cast]
theorem coe_iInf {ι : Sort*} [Nonempty ι] (f : ι → ℝ≥0) : (↑(iInf f) : ℝ≥0∞) = ⨅ a, ↑(f a) :=
  WithTop.coe_iInf (OrderBot.bddBelow _)

Похожие утверждения