English
There is an equivalence characterizing IsEmbedding( Sum.elim f g ).
Русский
Существует эквивалентность, описывающая IsEmbedding( Sum.elim f g ).
LaTeX
$$$\\text{IsEmbedding}(\\mathrm{Sum.elim}\ f\ g) \\iff \\bigl(\\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)})\\bigr)$$$
Lean4
theorem isEmbedding_sumElim :
IsEmbedding (Sum.elim f g) ↔
IsEmbedding f ∧ IsEmbedding g ∧ Disjoint (closure (range f)) (range g) ∧ Disjoint (range f) (closure (range g)) :=
by
simp_rw [isEmbedding_iff, isInducing_sumElim, Sum.elim_injective]
constructor
· intro ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, f_ne_g⟩⟩
exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
· intro ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))
