symm

Mathlib.Topology.UnitInterval

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

English

σ is the central symmetry of the unit interval, defined by σ(t) = 1 − t.

Русский

σ — центральная симметрия единичного интервала, определяется как σ(t) = 1 − t.

LaTeX

$$$$ \sigma: \text{unitInterval} \to \text{unitInterval},\quad \sigma(t)=1-t. $$$$

Lean4

/-- Unit interval central symmetry. -/
def symm : I → I := fun t => ⟨1 - t, Icc.mem_iff_one_sub_mem.mp t.prop⟩

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

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

Разделы

Аффилиация

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