equivMapDomain_trans' — Mathlib

English

EquivMapDomain (f.trans g) equals the composition of equivMapDomain g and equivMapDomain f as functions.

Русский

EquivMapDomain (f.trans g) равен композиции функций equivMapDomain g и equivMapDomain f.

LaTeX

$$equivMapDomain (f.trans g) = equivMapDomain g \\circ equivMapDomain f$$

Lean4

theorem equivMapDomain_trans' (f : α ≃ β) (g : β ≃ γ) :
    @equivMapDomain _ _ M _ (f.trans g) = equivMapDomain g ∘ equivMapDomain f := by ext x; rfl

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