piLpCurry_symm_apply — Mathlib

English

The symmetric (inverse) of the right congruence acts by applying inverses componentwise.

Русский

Обратное правого конгруента отображает координаты через обратные изометрии по каждой компоненте.

LaTeX

$$$(\text{piLpCongrRight}(p,e))^{-1}_{i} = e_i^{-1}$$$

Lean4

@[simp]
theorem _root_.LinearIsometryEquiv.piLpCurry_symm_apply (f : PiLp p (fun i => PiLp p (α i))) :
    (_root_.LinearIsometryEquiv.piLpCurry 𝕜 p α).symm f = toLp p (Sigma.uncurry fun i j => f i j) :=
  rfl

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