Iio_def

Mathlib.Order.Interval.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.Iio_def

English

Iio(a) is the set {x | x < a}.

Русский

Iio(a) — множество {x | x < a}.

LaTeX

$$$Iio(a) = \{x \mid x < a\}$$$

Lean4

theorem Iio_def (a : α) : {x | x < a} = Iio a :=
  rfl

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

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

Разделы

Аффилиация

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