English
If s is a neighborhood of π(a) in the codomain with the coinduced topology, then its preimage under π is a neighborhood of a in the domain.
Русский
Если s является окрестностью π(a) в кодоме с коиндукционной топологией, то его предобраз под π является окрестностью a в области.
LaTeX
$$$(s \in 𝓝(\pi(a))) \Rightarrow (\pi^{-1}(s) \in 𝓝(a))$$$
Lean4
theorem preimage_nhds_coinduced [TopologicalSpace α] {π : α → β} {s : Set β} {a : α}
(hs : s ∈ @nhds β (TopologicalSpace.coinduced π ‹_›) (π a)) : π ⁻¹' s ∈ 𝓝 a :=
by
letI := TopologicalSpace.coinduced π ‹_›
rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩
exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩
