toEquiv_uniformEquiv — Mathlib

English

The uniform equivalence between PiLp p β and the product space has the same underlying equivalence as WithLp.equiv.

Русский

Унитарное эквивалентное отображение между PiLp p β и произведением имеет то же основание эквивалентности, что и WithLp.equiv.

LaTeX

$$(uniformEquiv p β).toEquiv = WithLp.equiv p (Π i, β i)$$

Lean4

@[simp]
theorem toEquiv_uniformEquiv [∀ i, UniformSpace (β i)] : (uniformEquiv p β).toEquiv = WithLp.equiv p (Π i, β i) :=
  rfl

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