coe_sInf — Mathlib

English

If s is a nonempty subset of ℕ, then the coercion of its infimum to ENat equals the infimum taken over all elements of s, i.e., ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞).

Русский

Пусть s непусто; тогда приводимый к ENat нижний предел множества s равен нижнему пределу по элементам s: ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞).

LaTeX

$$$\uparrow(\mathrm{sInf}(s)) = \inf_{a \in s} (a : \mathbb{N}_\infty)$$$

Lean4

theorem coe_sInf (hs : s.Nonempty) : ↑(sInf s) = ⨅ a ∈ s, (a : ℕ∞) :=
  WithTop.coe_sInf hs (OrderBot.bddBelow s)

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