uniformity_basis_dist — Mathlib

English

The neighborhood basis at the unit 1 is given by ε-balls in norm: has basis { y : ‖y‖ < ε } around 1.

Русский

Базис окрестностей единицы состоит из ε-шаров по норме: имеет базис { y : ‖y‖ < ε } вокруг 1.

LaTeX

$$$\\big(\\mathcal{nhds}(1_E)\\big).HasBasis (\\lambda \\varepsilon: \\mathbb{R}, \\varepsilon > 0) (\\lambda \\varepsilon, y . \\|y\\| < \\varepsilon)$$$

Lean4

@[to_additive]
theorem uniformity_basis_dist : (𝓤 E).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {p : E × E | ‖p.fst / p.snd‖ < ε} :=
  by
  convert Metric.uniformity_basis_dist (α := E) using 1
  simp [dist_eq_norm_div]

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