sumElim — Mathlib

English

If f and g are open embeddings and Sum.elim f g is injective, then Sum.elim f g is an open embedding.

Русский

Если f и g — открытые вложения и Sum.elim f g инъективно, то Sum.elim f g является открытым вложением.

LaTeX

$$$$\\mathrm{IsOpenEmbedding}(\\mathrm{Sum.elim} f g) = \\text{ given } hf, hg, h \\implies \\text{open embedding}.$$$$

Lean4

theorem sumElim {f : X → Z} {g : Y → Z} (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g)
    (h : Injective (Sum.elim f g)) : IsOpenEmbedding (Sum.elim f g) :=
  by
  rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

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