symmHomeomorph — Mathlib

English

There exists a homeomorphism of the unit interval I onto itself given by σ, with σ(t) = 1 − t.

Русский

Существует гомеоморфизм единичного отрезка I в самого себя, заданный σ(t) = 1 − t.

LaTeX

$$$\sigma: I \to I,\ \sigma(t)=1-t,\ \sigma \in \mathrm{Homeo}(I)$$$

Lean4

/-- `unitInterval.symm` as a `Homeomorph`. -/
@[simps]
def symmHomeomorph : I ≃ₜ I where
  toFun := symm
  invFun := symm
  left_inv := symm_symm
  right_inv := symm_symm

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