English
The isInducing_sumElim theorem expresses an equivalence: Sum.elim f g is inducing iff f and g are inducing and the separation conditions hold.
Русский
Теорема isInducing_sumElim формулирует эквивалентность: Sum.elim f g индуктивно, если и только если f и g индуктивны и соблюдены условия разнесения.
LaTeX
$$$\\text{IsInducing}(\\mathrm{Sum.elim}\ f\ g) \\iff \\bigl(\\text{IsInducing}(f) \\wedge \\text{IsInducing}(g) \\wedge \\text{Disjoint}(\\overline{\\mathrm{range}(f)}, \\mathrm{range}(g)) \\wedge \\text{Disjoint}(\\mathrm{range}(f), \\overline{\\mathrm{range}(g)})\\bigr)$$$
Lean4
theorem isInducing_sumElim :
IsInducing (Sum.elim f g) ↔
IsInducing f ∧ IsInducing g ∧ Disjoint (closure (range f)) (range g) ∧ Disjoint (range f) (closure (range g)) :=
⟨fun h ↦
⟨h.sumElim_left, h.sumElim_right, h.disjoint_of_sumElim_aux,
((Sum.elim_swap ▸ h.comp IsInducing.sumSwap).disjoint_of_sumElim_aux).symm⟩,
fun ⟨hf, hg, hFg, hfG⟩ ↦ hf.sumElim hg hFg hfG⟩
