piLpCongrRight_symm — Mathlib

English

A specialized congruenceRight action changing only one coordinate isometrically is equivalent to applying the corresponding isometry to that coordinate.

Русский

Специализированное правое конгруентное отображение, меняющее только одну координату изометрически, эквивалентно применению изометрии к этой координате.

LaTeX

$$$\text{LinearIsometryEquiv.piLpCongrRightSingle}(p,e,i,v) = \text{toLp}(p,\Pi.single i (e_i(v)))$$$

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.piLpCongrRight_symm (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) :
    (LinearIsometryEquiv.piLpCongrRight p e).symm = LinearIsometryEquiv.piLpCongrRight p (fun i => (e i).symm) :=
  rfl

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