uniformity_basis_dist_inv_nat_pos

English

There is a basis of the uniformity indexed by natural numbers n with entourages { (a,b) | dist(a,b) < 1/n } for n large enough (positive).

Русский

Существует база униформности, индексируемая по натуральным числам n с окружностями { (a,b) | dist(a,b) < 1/n } для больших n.

LaTeX

$$$$ (\\mathcal{U}(\\alpha)) \\HasBasis (n: \\mathbb{N}) \\bigl( n \\mapsto \\{ (a,b) \\in \\alpha \\times \\alpha \\mid \\operatorname{dist}(a,b) < 1/n \\} \\bigr) $$$$

Lean4

theorem uniformity_basis_dist_inv_nat_pos :
    (𝓤 α).HasBasis (fun n : ℕ => 0 < n) fun n : ℕ => {p : α × α | dist p.1 p.2 < 1 / ↑n} :=
  Metric.mk_uniformity_basis (fun _ hn => div_pos zero_lt_one <| Nat.cast_pos.2 hn) fun _ ε0 =>
    let ⟨n, hn⟩ := exists_nat_one_div_lt ε0
    ⟨n + 1, Nat.succ_pos n, mod_cast hn.le⟩

Похожие утверждения