punctured_nhds_module_neBot — Mathlib

English

If E is a nontrivial normed space over a real field and r ≥ 0, then the sphere centered at 0 with radius r is nonempty in a compatible RCLike context.

Русский

Если E — ненулевое нормированное пространство над реалевым полем, и радиус r неотрицателен, сфера радиуса r ненулевая.

LaTeX

$$$\\text{Nonempty}(\\text{sphere}(0, r))$$$

Lean4

/-- If `E` is a nontrivial topological module over `ℝ`, then `E` has no isolated points.
This is a particular case of `Module.punctured_nhds_neBot`. -/
instance punctured_nhds_module_neBot {E : Type*} [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Nontrivial E]
    [Module ℝ E] [ContinuousSMul ℝ E] (x : E) : NeBot (𝓝[≠] x) :=
  Module.punctured_nhds_neBot ℝ E x

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