skewProd_symm_apply — Mathlib

English

The inverse of the skew product acts by the formula (e.symm(x1), e'.symm(x2 − f(e.symm(x1)))).

Русский

Обратное skewProd действует по формуле (e.symm(x1), e'.symm(x2 − f(e.symm(x1)))).

LaTeX

$$$ (e.skewProd e' f)^{-1} \, x = (e^{-1}(x_1), e'^{-1}(x_2 - f(e^{-1}(x_1)))) $$$

Lean4

@[simp]
theorem skewProd_symm_apply (e : M ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (f : M →L[R] M₄) (x) :
    (e.skewProd e' f).symm x = (e.symm x.1, e'.symm (x.2 - f (e.symm x.1))) :=
  rfl

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