prodUnique — Mathlib

English

The action of prodUnique on a pair (n,m) sends it to m.

Русский

Действие prodUnique на паре (n,m) отправляет её в m.

LaTeX

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

Lean4

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

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