_example

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#Tactic.Interactive._example

English

The map x ↦ a x + b sends the unit interval [0,1] homeomorphically onto [b, a+b] for a>0.

Русский

Отображение x ↦ a x + b (при a>0) переводит единичный интервал [0,1] гомеоморфно в отрезок [b, a+b].

LaTeX

$$affineHomeomorph a b h.ne.symm '' Set.Icc 0 1 = Set.Icc b (a + b)$$

Lean4

example (x : unitInterval) : 0 ≤ (x : ℝ) := by unit_interval

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

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

Разделы

Аффилиация

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