piLpCongrRight_single — Mathlib

English

The action of congrRightSingle on a pure single-coordinate element is given by applying the corresponding isometry to that coordinate.

Русский

Действие CongrRightSingle на элемент, полученный одной координатой, задаётся применением изометрии к этой координате.

LaTeX

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

Lean4

@[simp high]
theorem _root_.LinearIsometryEquiv.piLpCongrRight_single (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) [DecidableEq ι] (i : ι) (v : α i) :
    LinearIsometryEquiv.piLpCongrRight p e (toLp p <| Pi.single i v) = toLp p (Pi.single i (e _ v)) :=
  funext <| Pi.apply_single (e ·) (fun _ => map_zero _) _ _

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