English
Let R be a topological ring with no isolated zero, and let M be a nontrivial R-module with the property that c·x = 0 implies c = 0 or x = 0. Then every point of M is non-isolated in the punctured neighborhood: for all x ∈ M, the punctured neighborhood 𝓝[≠] x is nonempty.
Русский
Пусть R — топологическая кольцо без изолированного нуля, M — ненулевой модуль над R, такой что c·x = 0 ⇒ c = 0 или x = 0. Тогда в M нет изолированных точек: для каждого x ∈ M непусто собственное punctured окрестности 𝓝[≠] x.
LaTeX
$$$\forall x \in M,\; \mathcal{N}_{x}^{\neq} \neq \varnothing,$ where $\mathcal{N}_{x}^{\neq}=\mathcal{N}(x)\cap\{y\mid y\neq x\}$.$$
Lean4
/-- Let `R` be a topological ring such that zero is not an isolated point (e.g., a nontrivially
normed field, see `NormedField.punctured_nhds_neBot`). Let `M` be a nontrivial module over `R`
such that `c • x = 0` implies `c = 0 ∨ x = 0`. Then `M` has no isolated points. We formulate this
using `NeBot (𝓝[≠] x)`.
This lemma is not an instance because Lean would need to find `[ContinuousSMul ?m_1 M]` with
unknown `?m_1`. We register this as an instance for `R = ℝ` in `Real.punctured_nhds_module_neBot`.
One can also use `haveI := Module.punctured_nhds_neBot R M` in a proof.
-/
theorem punctured_nhds_neBot [Nontrivial M] [NeBot (𝓝[≠] (0 : R))] [NoZeroSMulDivisors R M] (x : M) : NeBot (𝓝[≠] x) :=
by
rcases exists_ne (0 : M) with ⟨y, hy⟩
suffices Tendsto (fun c : R => x + c • y) (𝓝[≠] 0) (𝓝[≠] x) from this.neBot
refine Tendsto.inf ?_ (tendsto_principal_principal.2 <| ?_)
· convert tendsto_const_nhds.add ((@tendsto_id R _).smul_const y)
rw [zero_smul, add_zero]
· intro c hc
simpa [hy] using hc
