extendDomain_trans — Mathlib

English

The extendDomain operation respects composition: (e.extendDomain f) trans (e'.extendDomain f) = Perm.extendDomain (e trans e') f.

Русский

Операция extendDomain сохраняет композицию: (e.extendDomain f) .trans (e'.extendDomain f) = Perm.extendDomain (e trans e') f.

LaTeX

$$$(e.extendDomain f).trans (e'.extendDomain f) = Perm.extendDomain (e \\circ e') f$$$

Lean4

theorem extendDomain_trans (e e' : Perm α') :
    (e.extendDomain f).trans (e'.extendDomain f) = Perm.extendDomain (e.trans e') f := by
  simp [Perm.extendDomain, permCongr_trans]

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