isOpenMap_sumElim — Mathlib

English

The map Sum.elim f g is an open embedding provided f and g are open embeddings and Sum.elim f g is injective.

Русский

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

LaTeX

$$$$\\mathrm{IsOpenEmbedding}(\\mathrm{Sum.elim} f g) \\text{ under suitable hypotheses } hf, hg, h.$$$$

Lean4

@[simp]
theorem isOpenMap_sumElim {f : X → Z} {g : Y → Z} : IsOpenMap (Sum.elim f g) ↔ IsOpenMap f ∧ IsOpenMap g := by
  simp only [isOpenMap_sum, elim_inl, elim_inr]

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