English
Any nonempty Polish space α admits a continuous surjection f:(ℕ→ℕ)→α.
Русский
Любое непустое полишпространство α имеет непрерывное сюръективное отображение f:(ℕ→ℕ)→α.
LaTeX
$$$$\\\\exists f:(\\\\mathbb{N}\\\\rightarrow\\\\mathbb{N})\\\\rightarrow α, \\\\text{Continuous } f \\\\land \\\\text{Surjective } f.$$$$
Lean4
/-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`,
defining the right topology and uniform structure. It is highly non-canonical, though, and therefore
not registered as a global instance.
The distance we use here is `dist x y = ∑' n, min (1/2)^(encode i) (dist (x n) (y n))`. -/
protected def metricSpace : MetricSpace (∀ i, F i)
where
dist_self x := by simp [dist_eq_tsum]
dist_comm x y := by simp [dist_eq_tsum, dist_comm]
dist_triangle x y
z :=
have I :
∀ i,
min ((1 / 2) ^ encode i : ℝ) (dist (x i) (z i)) ≤
min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) + min ((1 / 2) ^ encode i : ℝ) (dist (y i) (z i)) :=
fun i =>
calc
min ((1 / 2) ^ encode i : ℝ) (dist (x i) (z i)) ≤
min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i) + dist (y i) (z i)) :=
min_le_min le_rfl (dist_triangle _ _ _)
_ =
min ((1 / 2) ^ encode i : ℝ)
(min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) + min ((1 / 2) ^ encode i : ℝ) (dist (y i) (z i))) :=
by
convert
congr_arg ((↑) : ℝ≥0 → ℝ)
(min_add_distrib ((1 / 2 : ℝ≥0) ^ encode i) (nndist (x i) (y i)) (nndist (y i) (z i)))
_ ≤ min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) + min ((1 / 2) ^ encode i : ℝ) (dist (y i) (z i)) :=
min_le_right _ _
calc
dist x z ≤
∑' i, (min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) + min ((1 / 2) ^ encode i : ℝ) (dist (y i) (z i))) :=
(dist_summable x z).tsum_le_tsum I ((dist_summable x y).add (dist_summable y z))
_ = dist x y + dist y z := (dist_summable x y).tsum_add (dist_summable y z)
eq_of_dist_eq_zero
hxy := by
ext1 n
rw [← dist_le_zero, ← hxy]
apply dist_le_dist_pi_of_dist_lt
rw [hxy]
simp
toUniformSpace := Pi.uniformSpace _
uniformity_dist :=
by
simp only [Pi.uniformity, comap_iInf, gt_iff_lt, preimage_setOf_eq, comap_principal,
PseudoMetricSpace.uniformity_dist]
apply le_antisymm
· simp only [le_iInf_iff, le_principal_iff]
intro ε εpos
classical
obtain ⟨K, hK⟩ : ∃ K : Finset ι, (∑' i : { j // j ∉ K }, (1 / 2 : ℝ) ^ encode (i : ι)) < ε / 2 :=
((tendsto_order.1 (tendsto_tsum_compl_atTop_zero fun i : ι => (1 / 2 : ℝ) ^ encode i)).2 _
(half_pos εpos)).exists
obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ, 0 < δ ∧ (K.card : ℝ) * δ < ε / 2 := exists_pos_mul_lt (half_pos εpos) _
apply
@mem_iInf_of_iInter _ _ _ _ _ K.finite_toSet fun i =>
{p : (∀ i : ι, F i) × ∀ i : ι, F i | dist (p.fst i) (p.snd i) < δ}
· rintro ⟨i, hi⟩
refine mem_iInf_of_mem δ (mem_iInf_of_mem δpos ?_)
simp only [mem_principal, Subset.rfl]
· rintro ⟨x, y⟩ hxy
simp only [mem_iInter, mem_setOf_eq, SetCoe.forall, Finset.mem_coe] at hxy
calc
dist x y = ∑' i : ι, min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i)) := rfl
_ =
(∑ i ∈ K, min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i))) +
∑' i : ↑(K : Set ι)ᶜ, min ((1 / 2) ^ encode (i : ι) : ℝ) (dist (x i) (y i)) :=
(Summable.sum_add_tsum_compl (dist_summable _ _)).symm
_ ≤ (∑ i ∈ K, dist (x i) (y i)) + ∑' i : ↑(K : Set ι)ᶜ, ((1 / 2) ^ encode (i : ι) : ℝ) :=
by
gcongr
· apply min_le_right
· apply Summable.subtype (dist_summable x y) (↑K : Set ι)ᶜ
· apply Summable.subtype summable_geometric_two_encode (↑K : Set ι)ᶜ
· apply min_le_left
_ < (∑ _i ∈ K, δ) + ε / 2 := by
apply add_lt_add_of_le_of_lt _ hK
refine Finset.sum_le_sum fun i hi => (hxy i ?_).le
simpa using hi
_ ≤ ε / 2 + ε / 2 := by
gcongr
simpa using hδ.le
_ = ε := add_halves _
· simp only [le_iInf_iff, le_principal_iff]
intro i ε εpos
refine mem_iInf_of_mem (min ((1 / 2) ^ encode i : ℝ) ε) ?_
have : 0 < min ((1 / 2) ^ encode i : ℝ) ε := lt_min (by simp) εpos
refine mem_iInf_of_mem this ?_
simp only [and_imp, Prod.forall, setOf_subset_setOf, lt_min_iff, mem_principal]
intro x y hn hε
calc
dist (x i) (y i) ≤ dist x y := dist_le_dist_pi_of_dist_lt hn
_ < ε := hε
