isQuotientMap_of_isOpenQuotientMap_of_isInducing

English

If the diagram satisfies h, hf, hp, hq, hg, and H, then p is a quotient map.

Русский

Если диаграмма удовлетворяет условиям h, hf, hp, hq, hg и H, то p является квантом (квотирующим отображением).

LaTeX

$$$\mathrm{IsQuotientMap}(p)$$$

Lean4

theorem isQuotientMap_of_isOpenQuotientMap_of_isInducing (h : g ∘ p = q ∘ f) (hf : IsInducing f) (hp : Surjective p)
    (hq : IsOpenQuotientMap q) (hg : IsEmbedding g) (H : q ⁻¹' (q '' (Set.range f)) ⊆ Set.range f) : IsQuotientMap p :=
  ⟨hp,
    hg.eq_induced.trans
      ((coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing f g p q h hf hp hq hg.injective H)).symm⟩

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