liftIsometry_tprodL — Mathlib

English

The equality (liftIsometry 𝕜 E F) (tprodL 𝕜) = id expresses that the liftIsometry maps the canonical tensor generator to the identity.

Русский

Соблюдается равенство, что liftIsometry обходит tprodL и даёт тождество.

LaTeX

$$liftIsometry 𝕜 E F (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] i, E i)$$

Lean4

@[simp]
theorem liftIsometry_tprodL : liftIsometry 𝕜 E _ (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] i, E i) :=
  by
  ext _
  simp only [liftIsometry_apply_apply, tprodL_coe, lift_tprod, LinearMap.id_coe, id_eq, ContinuousLinearMap.coe_id']

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