piLpCongrLeft_apply — Mathlib

English

The value of the left congruence is exactly the functorial reindexing of coordinates.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.piLpCongrLeft_apply (e : ι ≃ ι') (v : PiLp p fun _ : ι => E) :
    LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e v = Equiv.piCongrLeft' (fun _ : ι => E) e v :=
  rfl

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