Theorems · Theorem · functional analysis

Module.punctured_nhds_neBot

∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [ContinuousAdd M] [inst_5 : Module R M] [ContinuousSMul R M] [IsDomain R] [Nontrivial M]
  [(nhdsWithin 0 {0}ᶜ).NeBot] [Module.IsTorsionFree R M] (x : M), (nhdsWithin x {x}ᶜ).NeBot

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.

Defined in

Mathlib.Topology.Algebra.Module.Basic

Cited by

0 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingTopologicalSpaceTopologicalSpaceAddCommGroupContinuousAddModuleContinuousSMulIsDomainNontrivialFilter.NeBotModule.IsTorsionFree