English
The filter totalLengthFilter has a basis given by ε-balls (ε>0) mapped to sets of finite E with total length less than ε.
Русский
Фильтр totalLengthFilter имеет базис, задаваемый ε-окружностями (ε>0) и множествами конечных E, для которых общая длина менее ε.
LaTeX
$$$\text{totalLengthFilter.HasBasis}(\lambda \varepsilon>0.0,\ {E: \mathbb{N} \times (\mathbb{N} \to \mathbb{R} \times \mathbb{R}) \mid \sum_{i< E.1} \operatorname{dist}(E.2 i).1 (E.2 i).2 < \varepsilon})$$$
Lean4
theorem hasBasis_totalLengthFilter :
totalLengthFilter.HasBasis (fun (ε : ℝ) => 0 < ε)
(fun (ε : ℝ) => {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}) :=
by
convert Filter.HasBasis.comap (α := ℝ) _ (nhds_basis_Ioo_pos _) using 1
ext ε E
simp only [mem_setOf_eq, zero_sub, zero_add, mem_preimage, mem_Ioo, iff_and_self]
suffices 0 ≤ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 by grind
exact Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)
