liftIsometry_apply_apply — Mathlib

English

The inverse of liftIsometry acts by composing with tprodL: (liftIsometry).symm l = l ∘ tprodL.

Русский

Обратное к liftIsometry действует через композицию с tprodL: (liftIsometry).symm l = l ∘ tprodL.

LaTeX

$$(liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜)$$

Lean4

@[simp]
theorem liftIsometry_apply_apply (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
    liftIsometry 𝕜 E F f x = lift f.toMultilinearMap x := by
  simp only [liftIsometry, LinearIsometryEquiv.coe_mk, liftEquiv_apply, LinearMap.mkContinuous_apply]

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