coe_sSup — Mathlib

English

If s is a subset of ℕ that is bounded above, then the coercion of its supremum to ENat equals the supremum taken over all elements of s, i.e., ↑(sSup s) = ⨆ a ∈ s, (a : ℕ∞).

Русский

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

LaTeX

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

Lean4

theorem coe_sSup : BddAbove s → ↑(sSup s) = ⨆ a ∈ s, (a : ℕ∞) :=
  WithTop.coe_sSup

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