Ioi_def

Mathlib.Order.Interval.Set.Defs

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

English

Ioi(a) is the set of all elements of α that are strictly greater than a.

Русский

Ioi(a) — множество элементов α, строго больших a.

LaTeX

$$$$ Ioi(a) = \{ x \in \alpha \mid a < x \}. $$$$

Lean4

theorem Ioi_def (a : α) : {x | a < x} = Ioi a :=
  rfl

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

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

Разделы

Аффилиация

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