nhds_basis_norm_lt — Mathlib

English

The neighborhoods of x have a basis consisting of sets { y | ‖y / x‖ < ε } for ε > 0.

Русский

Окрестности точки x имеют базис из множеств { y | ‖y/x‖ < ε } при ε > 0.

LaTeX

$$$(\\mathcal{N} x).HasBasis (\\lambda \\varepsilon: \\mathbb{R}, \\varepsilon > 0) (\\lambda \\varepsilon, y . \\|y / x\\| < \\varepsilon)$$$

Lean4

@[to_additive]
theorem nhds_basis_norm_lt (x : E) : (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {y | ‖y / x‖ < ε} :=
  by
  simp_rw [← ball_eq']
  exact Metric.nhds_basis_ball

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