toHomeomorph — Mathlib

English

Each time-slice ϕ t acts as a homeomorphism of α with inverse ϕ(-t).

Русский

Каждый срез времени ϕ t является гомеоморфизмом пространства α, обратный к ϕ(-t).

LaTeX

$$$\\varphi(t) \\in \\mathrm{Homeomorph}(\\alpha, \\alpha)\\quad\\text{и}\\quad (\\varphi(t))^{-1} = \\varphi(-t).$$$

Lean4

/-- The map `ϕ t` as a homeomorphism. -/
def toHomeomorph (t : τ) : (α ≃ₜ α) where
  toFun := ϕ t
  invFun := ϕ (-t)
  left_inv x := by rw [← map_add, neg_add_cancel, map_zero_apply]
  right_inv x := by rw [← map_add, add_neg_cancel, map_zero_apply]
  continuous_toFun := by fun_prop
  continuous_invFun := by fun_prop

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