coe_sInf — Mathlib

English

If s ⊆ ℝ≥0 is nonempty, the ENNReal of the infimum of s equals the infimum over s of the ENNReal images: ↑(sInf s) = ⨅ a∈s, ↑a.

Русский

Если s непусто, то ENNReal(Inf s) равен Inf изображений s в ENNReal: ↑(sInf s) = ⨅ a∈s, ↑a.

LaTeX

$$$$\\uparrow(\\mathrm{sInf}\\ s) = \\big(\\bigsqcap_{a \\in s} \\uparrow a\\bigsqcap\\big)$$$$

Lean4

theorem coe_sInf {s : Set ℝ≥0} (hs : s.Nonempty) : (↑(sInf s) : ℝ≥0∞) = ⨅ a ∈ s, ↑a :=
  WithTop.coe_sInf hs (OrderBot.bddBelow s)

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