English
For a map f: β → α and a subset s ⊆ β, s is a neighborhood of a in the induced topology on β iff there exists a neighborhood u of f(a) in α with f^{-1}(u) ⊆ s.
Русский
Для отображения f: β → α и подмножества s ⊆ β: s является окрестностью точки a в индуцированной топологии тогда и только тогда, когда существует окрестность u точки f(a) в α такая, что f^{-1}(u) ⊆ s.
LaTeX
$$$s \\in @nhds\\\\beta (TopologicalSpace.induced f T) a \\iff \\exists u \\in 𝓝 (f a),\\; f^{-1}(u) \\subseteq s.$$$
Lean4
theorem mem_nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) :
s ∈ @nhds β (TopologicalSpace.induced f T) a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s :=
by
letI := T.induced f
simp_rw [mem_nhds_iff, isOpen_induced_iff]
constructor
· rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
· rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩
