English
For a map f: Sigma σ → X, IsInducing f is equivalent to conditions that restrict f to each summand are inducing and the images of summands can be separated by open sets.
Русский
Для отображения f: Sigma σ → X being IsInducing эквивалентны условия, что restrictions f на каждую компоненту индуктивны, и изображения компонент можно разделить открытыми множествами.
LaTeX
$$$\\text{IsInducing}(f) \\iff (\\forall i,\\ IsInducing (f\\circ \\Sigma.mk\\ i)) \\land (\\forall i,\\ exists\ U,\ IsOpen(U) \\land \\forall x, f x \\in U \\leftrightarrow x.1 = i)$$$
Lean4
/-- A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological
spaces) is inducing iff its restriction to each component is inducing and each the image of each
component under `f` can be separated from the images of all other components by an open set. -/
theorem inducing_sigma {f : Sigma σ → X} :
IsInducing f ↔ (∀ i, IsInducing (f ∘ Sigma.mk i)) ∧ (∀ i, ∃ U, IsOpen U ∧ ∀ x, f x ∈ U ↔ x.1 = i) :=
by
refine ⟨fun h ↦ ⟨fun i ↦ h.comp IsEmbedding.sigmaMk.1, fun i ↦ ?_⟩, ?_⟩
· rcases h.isOpen_iff.1 (isOpen_range_sigmaMk (i := i)) with ⟨U, hUo, hU⟩
refine ⟨U, hUo, ?_⟩
simpa [Set.ext_iff] using hU
· refine fun ⟨h₁, h₂⟩ ↦ isInducing_iff_nhds.2 fun ⟨i, x⟩ ↦ ?_
rw [Sigma.nhds_mk, (h₁ i).nhds_eq_comap, comp_apply, ← comap_comap, map_comap_of_mem]
rcases h₂ i with ⟨U, hUo, hU⟩
filter_upwards [preimage_mem_comap <| hUo.mem_nhds <| (hU _).2 rfl] with y hy
simpa [hU] using hy
