lowerClosure_singleton

Mathlib.Order.UpperLower.Closure

URI: https://scilib.ai/kg/mathlib#lowerClosure_singleton

English

The lower closure of a singleton {a} is the principal down-set {x : x ≤ a}.

Русский

Нижнее замыкание одинокого элемента {a} равно множеству элементов меньших или равных a.

LaTeX

$$$\mathrm{lowerClosure}(({a}) ) = \mathrm{LowerSet.Iic a}$$$

Lean4

@[simp]
theorem lowerClosure_singleton (a : α) : lowerClosure ({ a } : Set α) = LowerSet.Iic a :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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