Theorems · Theorem · general topology

cardinal_eq_of_mem_nhds

∀ {E : Type u_1} (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : AddGroup E]
  [inst_2 : MulActionWithZero 𝕜 E] [inst_3 : TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E}
  {x : E}, s ∈ nhds x → Cardinal.mk ↑s = Cardinal.mk E

In a topological vector space over a nontrivially normed field, any neighborhood of a point has the same cardinality as the whole space.

Defined in

Mathlib.Topology.Algebra.Module.Cardinality

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddGroupMulActionWithZeroTopologicalSpaceContinuousAddContinuousSMul