comp — Mathlib

English

comp behaves as expected: composition of EsakiaHoms is EsakiaHom.

Русский

композиция морфизмов Эзякия определяется как новый EsakiaHom.

LaTeX

$$$\\text{comp}: EsakiaHom(\\beta,\\gamma) \\to EsakiaHom(\\alpha,\\beta) \\to EsakiaHom(\\alpha,\\gamma)$$$

Lean4

/-- Composition of `EsakiaHom`s as an `EsakiaHom`. -/
def comp (g : EsakiaHom β γ) (f : EsakiaHom α β) : EsakiaHom α γ :=
  ⟨g.toContinuousOrderHom.comp f.toContinuousOrderHom, fun a b h₀ =>
    by
    obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
    obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
    exact ⟨b, h₂, rfl⟩⟩

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