Iio

Mathlib.Order.UpperLower.Principal

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

English

Strict principal lower set: the set Iio(a) equipped with the lower-set structure is a principal lower set.

Русский

Строгое главное нижнее множество: Iio(a) образует главное нижнее множество.

LaTeX

$$Iio(a) := { x ∈ α | x < a }$$

Lean4

/-- Strict principal lower set. `Set.Iio` as a lower set. -/
nonrec def Iio (a : α) : LowerSet α :=
  ⟨Iio a, isLowerSet_Iio a⟩

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

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

Разделы

Аффилиация

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