unique — Mathlib

English

If φ' is a linear map with the property that φ'(tprod f) = φ f for all f, then φ' = lift φ.

Русский

Если φ' линейное отображение такое, что φ'(tprod f) = φ f для всех f, то φ' = lift φ.

LaTeX

$$$$ \forall f, φ'(tprod(R,f)) = φ(f) \Rightarrow φ' = \text{lift } φ $$$$

Lean4

theorem unique {φ' : (⨂[R] i, s i) →ₗ[R] E} (H : ∀ f, φ' (PiTensorProduct.tprod R f) = φ f) : φ' = lift φ :=
  lift.unique' (MultilinearMap.ext H)

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