iSup_Iic

Mathlib.Order.UpperLower.Closure

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

English

The supremum over a ∈ s of LowerSet Iic a equals the lower closure of s.

Русский

Супремум по a ∈ s LowerSet Iic a равен нижнему замыканию s.

LaTeX

$$$\\\\supsup_{a \\in s}\\\\, LowerSet.Iic a = lowerClosure s$$$

Lean4

@[simp]
theorem iSup_Iic (s : Set α) : ⨆ a ∈ s, LowerSet.Iic a = lowerClosure s :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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