unitInterval

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval

English

The unit interval is the closed interval [0,1] in the real numbers.

Русский

Единичный интервал — это замкнутый интервал [0,1] на вещественных числах.

LaTeX

$$$$ \text{unitInterval} = \{ x \in \mathbb{R} : 0 \le x \le 1 \}. $$$$

Lean4

/-- The unit interval `[0,1]` in ℝ. -/
abbrev unitInterval : Set ℝ :=
  Set.Icc 0 1

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

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

Разделы

Аффилиация

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