English
If each X_n is separable, then the inductive limit is a separable space.
Русский
Если каждый X_n сепарабелен, то индуктивный предел — сепарабельно пространство.
LaTeX
$$$\bigl(\forall n,\; \text{Separable}(X_n)\bigr) \Rightarrow \text{Separable}(\operatorname{InductiveLimit}(I))$$$
Lean4
theorem separableSpaceInductiveLimit_of_separableSpace {X : ℕ → Type u} [(n : ℕ) → MetricSpace (X n)]
[hs : (n : ℕ) → TopologicalSpace.SeparableSpace (X n)] {f : (n : ℕ) → X n → X (n + 1)}
(I : ∀ (n : ℕ), Isometry (f n)) : TopologicalSpace.SeparableSpace (Metric.InductiveLimit I) :=
by
choose hsX hcX hdX using (fun n ↦ TopologicalSpace.exists_countable_dense (X n))
let s := ⋃ (i : ℕ), (toInductiveLimit I i '' (hsX i))
refine ⟨s, countable_iUnion (fun n => (hcX n).image _), ?_⟩
refine .of_closure <| (dense_iUnion_range_toInductiveLimit I).mono <| iUnion_subset fun i ↦ ?_
calc
range (toInductiveLimit I i) ⊆ closure (toInductiveLimit I i '' (hsX i)) :=
(toInductiveLimit_isometry I i |>.continuous).range_subset_closure_image_dense (hdX i)
_ ⊆ closure s := closure_mono <| subset_iUnion (fun j ↦ toInductiveLimit I j '' hsX j) i
