English
Given f: X → Y and a topology on Y, the induced topology on X is the coarsest topology making f continuous; a set U is open in X iff U = f⁻¹(V) for some open V in Y.
Русский
Дана функция f: X → Y и топология на Y; индуцированная топология на X — наименьшая топология, делающая f непрерывной; множество U открыто в X тогда и только тогда, существует открытое V в Y с U = f⁻¹(V).
LaTeX
$$$IsOpen_X(s) \iff \exists t, IsOpen_Y(t) \land f^{-1}(t) = s$$$
Lean4
/-- Given `f : X → Y` and a topology on `Y`,
the induced topology on `X` is the collection of sets
that are preimages of some open set in `Y`.
This is the coarsest topology that makes `f` continuous. -/
def induced (f : X → Y) (t : TopologicalSpace Y) : TopologicalSpace X
where
IsOpen s := ∃ t, IsOpen t ∧ f ⁻¹' t = s
isOpen_univ := ⟨univ, isOpen_univ, preimage_univ⟩
isOpen_inter := by
rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩
exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩
isOpen_sUnion S
h := by
choose! g hgo hfg using h
refine ⟨⋃₀ (g '' S), isOpen_sUnion <| forall_mem_image.2 hgo, ?_⟩
rw [preimage_sUnion, biUnion_image, sUnion_eq_biUnion]
exact iUnion₂_congr hfg
