English
The evaluation of the coe of the flipMultilinearEquiv equals the corresponding evaluation of the flipped map.
Русский
Значение перехода к flipMultilinearEquiv равно значению перевернутого отображения.
LaTeX
$$$ (flipMultilinearEquiv 𝕜 E G G') f = f.flipLinear $$$
Lean4
theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : ∀ i, E i ≃ₗᵢ[𝕜] E₁ i) :
‖g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)‖ = ‖g‖ :=
by
apply le_antisymm (g.norm_compContinuous_linearIsometry_le fun i => (f i).toLinearIsometry)
have :
g =
(g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap fun i =>
((f i).symm : E₁ i →L[𝕜] E i) :=
by
ext1 m
simp only [compContinuousLinearMap_apply, LinearIsometryEquiv.coe_coe'', LinearIsometryEquiv.apply_symm_apply]
conv_lhs => rw [this]
apply
(g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).norm_compContinuous_linearIsometry_le fun i =>
(f i).symm.toLinearIsometry
