skewProd_apply

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.skewProd_apply

English

The action of a skew product on a pair (x, y) is given by (e(x), e'(y) + f(x)).

Русский

Действие skew product на пару (x, y) задаётся как (e(x), e'(y) + f(x)).

LaTeX

$$$ e.skewProd\, e'\\, f\\, x = (e\,x.1, e'\\, x.2 + f\\, x.1) $$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru