comp — Mathlib

English

Composition of continuous order homomorphisms yields another continuous order homomorphism; the action is the composition of underlying functions.

Русский

Состав двух непрерывных отображений, сохраняющих порядок, образует ещё одно такое отображение; действие — это композиция функций.

LaTeX

$$$\text{ContinuousOrderHom.comp}(f,g) : \alpha \toCo \gamma$ is defined by the underlying function $f \circ g$$$

Lean4

/-- Composition of `ContinuousOrderHom`s as a `ContinuousOrderHom`. -/
def comp (f : β →Co γ) (g : α →Co β) : ContinuousOrderHom α γ :=
  ⟨f.toOrderHom.comp g.toOrderHom, f.continuous_toFun.comp g.continuous_toFun⟩

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