English
Sum.elim f g is a closed embedding if f and g are closed embeddings and the induced map is injective.
Русский
Sum.elim f g — замкнутое вложение, если f и g — замкнутые вложения и Sum.elim f g инъективно.
LaTeX
$$$$\\mathrm{IsClosedEmbedding}(\\mathrm{Sum.elim} f g)$$ under the hypotheses.$$
Lean4
theorem sumElim {f : X → Z} {g : Y → Z} (hf : IsClosedEmbedding f) (hg : IsClosedEmbedding g)
(h : Injective (Sum.elim f g)) : IsClosedEmbedding (Sum.elim f g) :=
by
rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
exact
⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩
-- Homeomorphisms between the various constructions: sums of two homeomorphisms,
-- as well as commutativity, associativity and distributivity with products.
