of_comp — Mathlib

English

If f and g are continuous and IsQuotientMap (g ∘ f), then IsQuotientMap g.

Русский

Если f и g непрерывны и IsQuotientMap (g ∘ f), то IsQuotientMap g.

LaTeX

$$$\text{Continuous}(f) \rightarrow \text{Continuous}(g) \rightarrow \mathrm{IsQuotientMap}(\mathrm{Function\;Comp}(g,f)) \rightarrow \mathrm{IsQuotientMap}(g)$$$

Lean4

protected theorem of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsQuotientMap (g ∘ f)) : IsQuotientMap g :=
  ⟨hgf.1.of_comp, le_antisymm (by grw [hgf.eq_coinduced, ← coinduced_compose, hf.coinduced_le]) hg.coinduced_le⟩

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