trans — Mathlib

English

Applying the composition on a point equals applying the second then the first.

Русский

Применение композиции к точке равно последовательному применению второго, затем первого отображения.

LaTeX

$$$\bigl((e: P_1 \to P_2) \circ (e': P_2 \to P_3)\bigr)(p) = e'(e(p))$$$

Lean4

/-- Composition of two `ContinuousAffineEquiv`alences, applied left to right. -/
@[trans]
def trans (e : P₁ ≃ᴬ[k] P₂) (e' : P₂ ≃ᴬ[k] P₃) : P₁ ≃ᴬ[k] P₃
    where
  toAffineEquiv := e.toAffineEquiv.trans e'.toAffineEquiv
  continuous_toFun := e'.continuous_toFun.comp (e.continuous_toFun)
  continuous_invFun := e.continuous_invFun.comp (e'.continuous_invFun)

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