sSup_eq_iSup' — Mathlib

English

If α has a SupSet structure, then sSup s equals the iSup over the subtype elements: sSup s = ⨆ a : s, (a : α).

Русский

Если у α есть структура SupSet, то sSup s равен iSup над элементами-подмножествами: sSup s = ⨆ a : s, (a : α).

LaTeX

$$$$ \operatorname{sSup} s = \bigvee_{a : s} (a : \alpha) $$$$

Lean4

theorem sSup_eq_iSup' (s : Set α) : sSup s = ⨆ a : s, (a : α) := by rw [iSup, Subtype.range_coe]

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