comp — Mathlib

English

The composition of open quotient maps is an open quotient map.

Русский

Сложение открытых факторных отображений есть открытое факторное отображение.

LaTeX

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

Lean4

theorem comp {g : Y → Z} (hg : IsOpenQuotientMap g) (hf : IsOpenQuotientMap f) : IsOpenQuotientMap (g ∘ f) :=
  ⟨.comp hg.1 hf.1, .comp hg.2 hf.2, .comp hg.3 hf.3⟩

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