coe_comp_pseudoEpimorphism — Mathlib

English

The coercion of a composition to a pseudo-epimorphism equals the composition of the coerced components.

Русский

Приведение композиции к псевдоэпиморфизму совпадает с композицией приведённых компонентов.

LaTeX

$$$(g\\circ f: EsakiaHom) :\\; PseudoEpimorphism\\;\\alpha\\to\\gamma = (g: PseudoEpimorphism\\;\\beta\\to\\gamma) \\circ (f: PseudoEpimorphism\\;\\alpha\\to\\beta)$$$

Lean4

@[simp]
theorem coe_comp_pseudoEpimorphism (g : EsakiaHom β γ) (f : EsakiaHom α β) :
    (g.comp f : PseudoEpimorphism α γ) = (g : PseudoEpimorphism β γ).comp f :=
  rfl

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