toEquiv_homeomorphProd — Mathlib

English

The underlying equivalence of the homeomorphism equals the canonical equivalence WithLp.equiv p (α × β).

Русский

Элемент эквивалентности под гомеоморфизмом совпадает с каноническим эквивалентом WithLp.equiv p (α × β).

LaTeX

$$$$ (\\text{homeomorphProd } p \\ α \\ β).toEquiv = WithLp.equiv p (α × β) $$$$

Lean4

@[simp]
theorem toEquiv_homeomorphProd : (homeomorphProd p α β).toEquiv = WithLp.equiv p (α × β) :=
  rfl

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