English
If f is an inducing map between topological spaces and s is a separable subset of the target, then its preimage f^{-1}(s) is separable in the domain.
Русский
Если f — индуктивное отображение между пространствами и s — сепарабельное подмножество целевого пространства, то прообраз f^{-1}(s) по этому отображению сепарабелен в области определения.
LaTeX
$$$\\forall f\\, s\\,\\big(\\text{IsInducing } f \\big)\\; (\\text{IsSeparable } s) \\Rightarrow \\text{IsSeparable } (f^{-1}[s])$$$
Lean4
/-- The preimage of a separable set by an inducing map is separable. -/
protected theorem isSeparable_preimage {f : β → α} [TopologicalSpace β] (hf : IsInducing f) {s : Set α}
(hs : IsSeparable s) : IsSeparable (f ⁻¹' s) :=
by
have : SeparableSpace s := hs.separableSpace
have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _
have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) := (hf.comp IsInducing.subtypeVal).codRestrict _
have := this.secondCountableTopology
exact .of_subtype _
