appendHomeomorph — Mathlib

English

The toEquiv component of the Fin.appendHomeomorph matches Fin.appendEquiv.

Русский

Компоненту toEquiv гомеоморфизма Fin.appendHomeomorph соответствует Fin.appendEquiv.

LaTeX

$$$ (Fin.appendHomeomorph (X := X) m n).toEquiv = Fin.appendEquiv m n. $$$

Lean4

/-- The natural homeomorphism between `(Fin m → X) × (Fin n → X)` and `Fin (m + n) → X`.
`Fin.appendEquiv` as a homeomorphism -/
@[simps!]
def _root_.Fin.appendHomeomorph (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X)
    where
  toEquiv := Fin.appendEquiv m n
  continuous_toFun := Fin.continuous_append m n
  continuous_invFun := by
    rw [Fin.appendEquiv_eq_homeomorph]
    exact Homeomorph.continuous_invFun _

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