English
If Sum.elim f g is an inducing map, then the left component f is inducing.
Русский
Если Sum.elim f g является индуктивным отображением, то отображение f слева является индуктивным.
LaTeX
$$$\\text{IsInducing}(\\mathrm{Sum.elim}\ f\ g) \\Rightarrow \\text{IsInducing}(f)$$$
Lean4
/-- If `Sum.elim f g` is inducing, `closure (range f)` and `range g` must be disjoint.
This is an auxiliary result towards proving `isInducing_sumElim`. -/
theorem disjoint_of_sumElim_aux (h : IsInducing (Sum.elim f g)) : Disjoint (closure (range f)) (range g) :=
by
rcases h.isClosed_iff.mp isClosed_range_inl with ⟨C, C_closed, hC⟩
have A : closure (range f) ⊆ C := by
rw [C_closed.closure_subset_iff, ← elim_comp_inl f g, range_comp, image_subset_iff, hC]
have B : Disjoint C (range g) :=
by
rw [← image_univ, disjoint_image_right, ← elim_comp_inr f g, preimage_comp, hC, ← disjoint_image_right, ←
image_univ]
exact disjoint_image_inl_image_inr
exact B.mono_left A
