English
If Sum.elim f g is an inducing map, then so are f and g, with the separating property between the ranges: the closure of range f is disjoint from range g, and range f is disjoint from the closure of range g.
Русский
Если Sum.elim f g является индуктивным отображением, то и f, и g таковыми являются, причём замыкание множества образов f и множество образов g разособлены: closure(range f) ∩ range g = ∅ и range f ∩ closure(range g) = ∅.
LaTeX
$$$\\text{IsInducing}(\\mathrm{Sum.elim}\ f\ g) \\Rightarrow (\\mathrm{IsInducing}\ f) \\,\\land\\, (\\mathrm{IsInducing}\ g) \\,\\land\\, \\overline{\\mathrm{range}(f)} \\cap \\mathrm{range}(g) = \\varnothing \\,\\land\\, \\mathrm{range}(f) \\cap \\overline{\\mathrm{range}(g)} = \\varnothing$$$
Lean4
/-- If `f` and `g` are inducing maps whose ranges are separated, then `Sum.elim f g` is inducing. -/
theorem sumElim (hf : IsInducing f) (hg : IsInducing g) (hFg : Disjoint (closure (range f)) (range g))
(hfG : Disjoint (range f) (closure (range g))) : IsInducing (Sum.elim f g) :=
by
rw [← disjoint_principal_nhdsSet] at hFg
rw [← disjoint_nhdsSet_principal] at hfG
rw [isInducing_iff_nhds]
intro x
apply le_antisymm ((hf.continuous.sumElim hg.continuous).tendsto x).le_comap
obtain x | x := x <;>
simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap, ← hg.nhds_eq_comap,
sup_le_iff, le_rfl, true_and, and_true] <;>
convert bot_le (α := Filter (X ⊕ Y)) <;>
rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]
· rw [← disjoint_principal_right]
exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))
· rw [← disjoint_principal_left]
exact hFg.mono_right (nhds_le_nhdsSet (mem_range_self x))
