qRight_one_right

Mathlib.Topology.Homotopy.HSpaces

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

English

For every t in I, qRight((t, 1)) = t.

Русский

Для каждого t ∈ I выполняется qRight((t,1)) = t.

LaTeX

$$$\forall t\in I,\ qRight(t,1)=t$$$

Lean4

theorem qRight_one_right (t : I) : qRight (t, 1) = t :=
  Eq.trans (by rw [qRight]; norm_num) <| Set.projIcc_val zero_le_one _

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

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

Разделы

Аффилиация

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