coe_sSup

Mathlib.Order.CompleteSublattice

URI: https://scilib.ai/kg/mathlib#CompleteSublattice.coe_sSup

English

The α-value of the supremum of S is the supremum in α of the α-values of members of S.

Русский

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

LaTeX

$$$\forall S \subseteq L,\ (↑(sSup S) : α) = sSup\{ (s : α) \mid s \in S\}$$$

Lean4

@[simp]
theorem coe_sSup (S : Set L) : (↑(sSup S) : α) = sSup ({(s : α) | s ∈ S}) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru