comp — Mathlib

English

The composition of quotient maps is a quotient map: if g and f are quotient maps, then g ∘ f is a quotient map.

Русский

Сложение факторизующих отображений является факторизующим: если g и f — факторизующие отображения, то g ∘ f — факторизующее отображение.

LaTeX

$$$\mathrm{IsQuotientMap}(g) \rightarrow \mathrm{IsQuotientMap}(f) \rightarrow \mathrm{IsQuotientMap}(g \circ f)$$$

Lean4

protected theorem comp (hg : IsQuotientMap g) (hf : IsQuotientMap f) : IsQuotientMap (g ∘ f) :=
  ⟨hg.surjective.comp hf.surjective, by rw [hg.eq_coinduced, hf.eq_coinduced, coinduced_compose]⟩

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