univ_eq_Icc

Mathlib.Topology.UnitInterval

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

English

The entire unit interval (as a subset) is equal to the closed interval [0,1].

Русский

Вся единичная интервал как множество равна замкнутому интервалу [0,1].

LaTeX

$$$$ \text{univ} = \text{Icc}(0,1). $$$$

Lean4

theorem univ_eq_Icc : (univ : Set I) = Icc (0 : I) (1 : I) :=
  Icc_bot_top.symm

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

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

Разделы

Аффилиация

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