equivMapDomain_trans — Mathlib

English

For f : α ≃ β, g : β ≃ γ, and l : α →₀ M, we have equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l).

Русский

Для f : α ≃ β, g : β ≃ γ и l : α →₀ M верно равенство equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l).

LaTeX

$$equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)$$

Lean4

theorem equivMapDomain_trans (f : α ≃ β) (g : β ≃ γ) (l : α →₀ M) :
    equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l) := by ext x; rfl

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