uniqueProd — Mathlib

English

The uniqueProd map sends a pair (n,m) to m.

Русский

Карта uniqueProd отправляет пару (n,m) в m.

LaTeX

$$$$ uniqueProd\, R\, M\, N (n,m) = m. $$$$

Lean4

/-- The natural equivalence `N × M ≃L[R] M` for any `Unique` type `N`.
This is `Equiv.uniqueProd` as a continuous linear equivalence. -/
def uniqueProd : (N × M) ≃L[R] M where
  toLinearEquiv := LinearEquiv.uniqueProd
  continuous_toFun := by
    change Continuous (Equiv.uniqueProd M N)
    dsimp; fun_prop
  continuous_invFun := by
    change Continuous fun x ↦ (default, x)
    fun_prop

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