English
The composition of two pseudo-epimorphisms g: β→γ and f: α→β is a pseudo-epimorphism α→γ, defined by composing their underlying order-homomorphisms, and it preserves the lifting property via the exists_map_eq_of_map_le' method.
Русский
Композиция двух псевдоэпиморфизмов g:β→γ и f:α→β есть псевдоэпиморфизм α→γ; он задаётся как композиция их отображений по порядку и сохраняет свойство восхождения через существование соответствующего отображения.
LaTeX
$$$\mathrm{comp}:\mathrm{PseudoEpimorphism}(\beta,\gamma) \to (\mathrm{PseudoEpimorphism}(\alpha,\beta) \to \mathrm{PseudoEpimorphism}(\alpha,\gamma))$; $(g,f)\mapsto g\circ f$$$
Lean4
/-- Composition of `PseudoEpimorphism`s as a `PseudoEpimorphism`. -/
def comp (g : PseudoEpimorphism β γ) (f : PseudoEpimorphism α β) : PseudoEpimorphism α γ :=
⟨g.toOrderHom.comp f.toOrderHom, 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⟩⟩
