coe_trans — Mathlib

English

The composition of two homeomorphisms corresponds to the composition of their associated continuous maps.

Русский

Складывание двух гомеоморфизмов соответствует композиции сопряжённых непрерывных отображений.

LaTeX

$$$(f.trans g : C(\\alpha,\\gamma)) = (g : C(\\beta,\\gamma)).\\text{comp } f$$$

Lean4

@[simp]
theorem coe_trans : (f.trans g : C(α, γ)) = (g : C(β, γ)).comp f :=
  rfl

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