English
The series ∑ min((1/2)^encode i, dist(x_i,y_i)) is summable.
Русский
Серия ∑ min((1/2)^{encode i}, dist(x_i,y_i)) сходится.
LaTeX
$$$$\\\\sum' i:ι, \\\\min((\\\\tfrac12)^{\\\\encode i}, dist(x_i,y_i)) \\\\text{ is summable}. $$$$
Lean4
protected theorem iInf {ι : Type*} [Countable ι] {t : ι → TopologicalSpace α} (ht₀ : ∃ i₀, ∀ i, t i ≤ t i₀)
(ht : ∀ i, @PolishSpace α (t i)) : @PolishSpace α (⨅ i, t i) :=
by
rcases ht₀ with ⟨i₀, hi₀⟩
rcases
CompletePseudometrizable.iInf
⟨t i₀,
letI := t i₀;
haveI := ht i₀;
inferInstance,
hi₀⟩
fun i ↦
letI := t i;
haveI := ht i;
letI := upgradeIsCompletelyMetrizable α
⟨inferInstance, inferInstance, inferInstance, rfl⟩ with
⟨u, hcomp, hcount, htop⟩
rw [← htop]
have : @SecondCountableTopology α u.toTopologicalSpace :=
htop.symm ▸
secondCountableTopology_iInf fun i ↦
letI := t i;
(ht i).toSecondCountableTopology
have : @T1Space α u.toTopologicalSpace :=
htop.symm ▸ t1Space_antitone (iInf_le _ i₀) (by letI := t i₀; haveI := ht i₀; infer_instance)
infer_instance
