Iic_def

Mathlib.Order.Interval.Set.Defs

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

English

Iic(b) is the set {x | x ≤ b}.

Русский

Iic(b) — множество {x | x ≤ b}.

LaTeX

$$$Iic(b) = \{x \mid x \le b\}$$$

Lean4

theorem Iic_def (b : α) : {x | x ≤ b} = Iic b :=
  rfl

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

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

Разделы

Аффилиация

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