qRight_zero_left

Mathlib.Topology.Homotopy.HSpaces

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

English

For every θ in I, qRight((0, θ)) = 0.

Русский

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

LaTeX

$$$\forall \theta \in I,\ qRight(0,\theta)=0$$$

Lean4

theorem qRight_zero_left (θ : I) : qRight (0, θ) = 0 :=
  Set.projIcc_of_le_left _ <| by simp only [coe_zero, mul_zero, zero_div, le_refl]

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

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

Разделы

Аффилиация

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