English
If α is second countable, then NonemptyCompacts α is second countable.
Русский
Если α вторично счетно, то NonemptyCompacts α вторично счетно.
LaTeX
$$$[\\text{SecondCountableTopology }\\alpha] \\Rightarrow \\text{SecondCountableTopology}(\\text{NonemptyCompacts }\\alpha).$$$
Lean4
/-- In a second countable space, the type of nonempty compact subsets is second countable -/
instance secondCountableTopology [SecondCountableTopology α] : SecondCountableTopology (NonemptyCompacts α) :=
haveI : SeparableSpace (NonemptyCompacts α) := by
/- To obtain a countable dense subset of `NonemptyCompacts α`, start from
a countable dense subset `s` of α, and then consider all its finite nonempty subsets.
This set is countable and made of nonempty compact sets. It turns out to be dense:
by total boundedness, any compact set `t` can be covered by finitely many small balls, and
approximations in `s` of the centers of these balls give the required finite approximation
of `t`. -/
rcases exists_countable_dense α with ⟨s, cs, s_dense⟩
let v0 := {t : Set α | t.Finite ∧ t ⊆ s}
let v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (t : Set α) ∈ v0}
refine ⟨⟨v, ?_, ?_⟩⟩
· have : v0.Countable := countable_setOf_finite_subset cs
exact this.preimage SetLike.coe_injective
· refine fun t =>
mem_closure_iff.2 fun ε εpos =>
?_
-- t is a compact nonempty set, that we have to approximate uniformly by a a set in `v`.
rcases exists_between εpos with ⟨δ, δpos, δlt⟩
have δpos' : 0 < δ / 2 := ENNReal.half_pos δpos.ne'
have Exy : ∀ x, ∃ y, y ∈ s ∧ edist x y < δ / 2 := by
intro x
rcases mem_closure_iff.1 (s_dense x) (δ / 2) δpos' with ⟨y, ys, hy⟩
exact ⟨y, ⟨ys, hy⟩⟩
let F x := (Exy x).choose
have Fspec : ∀ x, F x ∈ s ∧ edist x (F x) < δ / 2 := fun x => (Exy x).choose_spec
have : TotallyBounded (t : Set α) := t.isCompact.totallyBounded
obtain ⟨a : Set α, af : Set.Finite a, ta : (t : Set α) ⊆ ⋃ y ∈ a, ball y (δ / 2)⟩ :=
totallyBounded_iff.1 this (δ / 2) δpos'
let b := F '' a
have : b.Finite := af.image _
have tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ := by
intro x hx
rcases mem_iUnion₂.1 (ta hx) with ⟨z, za, Dxz⟩
exists F z, mem_image_of_mem _ za
calc
edist x (F z) ≤ edist x z + edist z (F z) := edist_triangle _ _ _
_ < δ / 2 + δ / 2 := (ENNReal.add_lt_add Dxz (Fspec z).2)
_ = δ :=
ENNReal.add_halves
_
-- keep only the points in `b` that are close to point in `t`, yielding a new set `c`
let c := {y ∈ b | ∃ x ∈ t, edist x y < δ}
have : c.Finite :=
‹b.Finite›.subset fun x hx =>
hx.1
-- points in `t` are well approximated by points in `c`
have tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ := by
intro x hx
rcases tb x hx with ⟨y, yv, Dxy⟩
have : y ∈ c := by simpa [c, -mem_image] using ⟨yv, ⟨x, hx, Dxy⟩⟩
exact
⟨y, this, le_of_lt Dxy⟩
-- points in `c` are well approximated by points in `t`
have ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ :=
by
rintro y ⟨_, x, xt, Dyx⟩
have : edist y x ≤ δ :=
calc
edist y x = edist x y := edist_comm _ _
_ ≤ δ := le_of_lt Dyx
exact
⟨x, xt, this⟩
-- it follows that their Hausdorff distance is small
have : hausdorffEdist (t : Set α) c ≤ δ := hausdorffEdist_le_of_mem_edist tc ct
have Dtc : hausdorffEdist (t : Set α) c < ε := this.trans_lt δlt
have hc : c.Nonempty :=
nonempty_of_hausdorffEdist_ne_top t.nonempty
(ne_top_of_lt Dtc)
-- let `d` be the version of `c` in the type `NonemptyCompacts α`
let d : NonemptyCompacts α := ⟨⟨c, ‹c.Finite›.isCompact⟩, hc⟩
have : c ⊆ s := by
intro x hx
rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨_, yx⟩⟩
rw [← yx]
exact (Fspec y).1
have : d ∈ v :=
⟨‹c.Finite›, this⟩
-- we have proved that `d` is a good approximation of `t` as requested
exact ⟨d, ‹d ∈ v›, Dtc⟩
UniformSpace.secondCountable_of_separable (NonemptyCompacts α)
