coe_sInf

Mathlib.Order.CompleteSublattice

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

English

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

Русский

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

LaTeX

$$$\left(\uparrow(\mathrm{sInf} S) : \alpha\right) = \mathrm{sInf}\{ (s : α) \mid s \in S\}$$$

Lean4

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

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

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

Разделы

Аффилиация

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