coe_sInf

Mathlib.Order.CompleteLatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iic.coe_sInf

English

The coe of sInf in Set.Iic a equals a ∧ sInf of the image.

Русский

Коe sInf в Set.Iic a равен a ∧ sInf образа.

LaTeX

$$$$ \uparrow(\operatorname{sInf} S) = a \wedge \operatorname{sInf}(\uparrow''S). $$$$

Lean4

@[simp]
theorem coe_sInf : (↑(sInf S) : α) = a ⊓ sInf ((↑) '' S) :=
  rfl

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

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

Разделы

Аффилиация

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