English
IsEmbedding(sElim f g) is equivalent to IsEmbedding f and IsEmbedding g with disjointness conditions.
Русский
IsEmbedding(Sum.elim f g) эквивалентно IsEmbedding f и IsEmbedding g с условиями разнесения.
LaTeX
$$$\\text{IsEmbedding}(\\mathrm{Sum.elim}\ f\ g) \\iff \\big( \\text{IsEmbedding}(f) \\wedge \\text{IsEmbedding}(g) \\wedge \\text{Disjoint}(\\overline{\\mathrm{range}(f)}, \\mathrm{range}(g)) \\wedge \\text{Disjoint}(\\mathrm{range}(f), \\overline{\\mathrm{range}(g)}) \\big)$$$
Lean4
/-- If `f` and `g` are embeddings whose ranges are separated, `Sum.elim f g` is an embedding. -/
theorem sumElim (hf : IsEmbedding f) (hg : IsEmbedding g) (hFg : Disjoint (closure (range f)) (range g))
(hfG : Disjoint (range f) (closure (range g))) : IsEmbedding (Sum.elim f g) :=
isEmbedding_sumElim.mpr ⟨hf, hg, hFg, hfG⟩
