changeForm_comp_changeForm — Mathlib

English

Two successive changes of form compose to the single change corresponding to the combined data.

Русский

Два последовательных перехода формы образуют один переход формы, соответствующий объединению данных.

LaTeX

$$$ (\text{changeForm}(h')).comp (\text{changeForm}(h)) = \text{changeForm}(\text{changeForm.add_proof}(h,h')) $$$

Lean4

theorem changeForm_comp_changeForm : (changeForm h').comp (changeForm h) = changeForm (changeForm.add_proof h h') :=
  LinearMap.ext <| changeForm_changeForm _ h'

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