coe_sInf

Mathlib.Order.UpperLower.CompleteLattice

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

English

For S ⊆ LowerSet α, the underlying set of sInf S equals ⋂ s ∈ S, s.

Русский

Пусть S — множество нижних множеств; основание sInf S равно ⋂ s∈S, s.

LaTeX

$$$ (↑(sInf S) : Set α) = ⋂ s ∈ S, ↑s $$$

Lean4

@[simp, norm_cast]
theorem coe_sInf (S : Set (LowerSet α)) : (↑(sInf S) : Set α) = ⋂ s ∈ S, ↑s :=
  rfl

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

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

Разделы

Аффилиация

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