coe_comp_continuousOrderHom — Mathlib

English

coe_comp_continuousOrderHom expresses that the underlying function of g∘f equals the composition of the underlying functions.

Русский

coe_comp_continuousOrderHom выражает, что базовая функция $(g\\circ f)$ равна композиции базовых функций $g$ и $f$.

LaTeX

$$$\\operatorname{toContinuousOrderHom}(g\\circ f) = (\\operatorname{toContinuousOrderHom}(g)) \\circ (\\operatorname{toContinuousOrderHom}(f))$$$

Lean4

@[simp]
theorem coe_comp_continuousOrderHom (g : EsakiaHom β γ) (f : EsakiaHom α β) :
    (g.comp f : α →Co γ) = (g : β →Co γ).comp f :=
  rfl

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