isEmbedding_of_isOpenQuotientMap_of_isInducing

English

If a diagram with inducing maps and open quotient maps satisfies the compatibility h and H, and g is injective, then g is an embedding.

Русский

Если диаграмма с индуктивными отображениями и открытыми квотирующими отображениями удовлетворяет условиям совместимости h и H, а g инъективна, тогда g является вложением (эмбеддингом).

LaTeX

$$$\mathrm{IsEmbedding}(g)$$$

Lean4

theorem isEmbedding_of_isOpenQuotientMap_of_isInducing (h : g ∘ p = q ∘ f) (hf : IsInducing f) (hp : IsQuotientMap p)
    (hq : IsOpenQuotientMap q) (hg : Function.Injective g) (H : q ⁻¹' (q '' (Set.range f)) ⊆ Set.range f) :
    IsEmbedding g :=
  ⟨⟨hp.eq_coinduced.trans (coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing f g p q h hf hp.surjective hq hg H)⟩,
    hg⟩

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