Ici_def

Mathlib.Order.Interval.Set.Defs

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

English

Ici(a) equals {x | a ≤ x}.

Русский

Ici(a) равно {x | a ≤ x}.

LaTeX

$$$Ici(a) = \{x \mid a \le x\}$$$

Lean4

theorem Ici_def (a : α) : {x | a ≤ x} = Ici a :=
  rfl

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

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

Разделы

Аффилиация

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