transAssocReparamAux_mem_I

Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

URI: https://scilib.ai/kg/mathlib#Path.Homotopy.transAssocReparamAux_mem_I

← MathLib Explorer

English

For every t in I, the value transAssocReparamAux(t) lies in the unit interval I.

Русский

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

LaTeX

$$$$\\mathrm{transAssocReparamAux}(t) \\in I.$$$$

Lean4

theorem transAssocReparamAux_mem_I (t : I) : transAssocReparamAux t ∈ I :=
  by
  unfold transAssocReparamAux
  split_ifs <;> constructor <;> linarith [unitInterval.le_one t, unitInterval.nonneg t]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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