piLpCongrLeft_single — Mathlib

English

The action of the left congruence on an element is explicitly given by the corresponding EquivLeft operation.

Русский

Действие левого конгруентного отображения на элемент явно задаётся соответствующей операцией EquivLeft.

LaTeX

$$$\text{LinearIsometryEquiv.piLpCongrLeft }(p,E,e)(v) = \text{Equiv.piCongrLeft'}(\ldots)(v)$$$

Lean4

@[simp high]
theorem _root_.LinearIsometryEquiv.piLpCongrLeft_single [DecidableEq ι] [DecidableEq ι'] (e : ι ≃ ι') (i : ι) (v : E) :
    LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e (toLp p <| Pi.single i v) = toLp p (Pi.single (e i) v) :=
  by
  funext x
  simp [LinearIsometryEquiv.piLpCongrLeft_apply, Equiv.piCongrLeft', Pi.single, Function.update, Equiv.symm_apply_eq]

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