Theorems · Theorem · general topology

cardinal_eq_of_isOpen

∀ {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},
  IsOpen s → s.Nonempty → Cardinal.mk ↑s = Cardinal.mk E

In a topological vector space over a nontrivially normed field, any nonempty open set has the same cardinality as the whole space.

Defined in

Mathlib.Topology.Algebra.Module.Cardinality

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddGroupMulActionWithZeroTopologicalSpaceContinuousAddContinuousSMul