piFinTwo — Mathlib

English

There is an isometry between (∀ i: Fin 2, α i) and α0 × α1.

Русский

Существует изометрия между (∀ i: Fin 2, α i) и α0 × α1.

LaTeX

$$$ (\forall i:Fin 2, α(i)) \simeq_i (α(0) \times α(1)) $$$

Lean4

/-- `piFinTwoEquiv` as an `IsometryEquiv`. -/
@[simps!]
def piFinTwo (α : Fin 2 → Type*) [∀ i, PseudoEMetricSpace (α i)] : (∀ i, α i) ≃ᵢ α 0 × α 1
    where
  toEquiv := piFinTwoEquiv α
  isometry_toFun x hx := by simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]

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