sumElim — Mathlib

English

If f and g are open embeddings, then Sum.elim f g is open embedding provided injectivity condition holds.

Русский

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

LaTeX

$$$$\\mathrm{IsOpenEmbedding}(\\mathrm{Sum.elim} f g) \\iff \\mathrm{IsOpenEmbedding} f \\land \\mathrm{IsOpenEmbedding} g.$$$$

Lean4

theorem sumElim {f : X → Z} {g : Y → Z} (hf : IsOpenMap f) (hg : IsOpenMap g) : IsOpenMap (Sum.elim f g) :=
  isOpenMap_sumElim.2 ⟨hf, hg⟩

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