genLoopHomeoOfIsEmpty — Mathlib

English

Reversal of a GenLoop along the i-th coordinate (symmetry along i).

Русский

Поворот GenLoop вдоль i-й координаты (симметрия по i).

LaTeX

$$$\\mathrm{symmAt}(i; f) = \\mathrm{copy}\\left(\\mathrm{fromLoop}\\; i\\ (\\mathrm{toLoop}\\; i\\ f).\\mathrm{symm}, \\; \\cdot \\right)$$$

Lean4

/-- The 0-dimensional generalized loops based at `x` are in bijection with `X`. -/
def genLoopHomeoOfIsEmpty (N x) [IsEmpty N] : Ω^ N X x ≃ₜ X
    where
  toFun f := f 0
  invFun y := ⟨ContinuousMap.const _ y, fun _ ⟨i, _⟩ => isEmptyElim i⟩
  left_inv f := by ext; exact congr_arg f (Subsingleton.elim _ _)
  continuous_invFun := ContinuousMap.const'.2.subtype_mk _

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