Theorems · Theorem · general topology

cardinal_eq_of_mem_nhds_zero

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

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

Defined in

Mathlib.Topology.Algebra.Module.Cardinality

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldZeroMulActionWithZeroTopologicalSpaceContinuousSMul