coe_sSup' — Mathlib

English

The α-value of the supremum of S equals the supremum over N ∈ S of N’s α-values.

Русский

Значение в α наибольшей границы множества S равно верхней границе по α элементов S.

LaTeX

$$$\left(\uparrow(\mathrm{sSup} S) : \alpha\right) = \bigvee_{N \in S} (N : \alpha)$$$

Lean4

theorem coe_sSup' (S : Set L) : (↑(sSup S) : α) = ⨆ N ∈ S, (N : α) := by rw [coe_sSup, ← Set.image, sSup_image]

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