toEquiv_uniformEquivProd — Mathlib

English

The underlying equivalence of uniformEquivProd p α β is the same as WithLp.equiv p (α × β).

Русский

Базовое эквивалентное отображение uniformEquivProd p α β совпадает с WithLp.equiv p (α × β).

LaTeX

$$$ (uniformEquivProd\, p\, \\alpha\, \\beta).toEquiv = WithLp.equiv\, p\, (\\alpha \\times \\beta). $$$

Lean4

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

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