English
In a topological vector space over a nontrivially normed field, a nonempty open set has the same cardinality as the whole space.
Русский
В топологическом векторном пространстве над ненулевым нормированным полем непустое открытое множество имеет ту же кардинальность, что и всё пространство.
LaTeX
$$$\\#s = \\#E$ for open nonempty $s$.$$
Lean4
/-- In a topological vector space over a nontrivially normed field, any nonempty open set has
the same cardinality as the whole space. -/
theorem cardinal_eq_of_isOpen {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [AddGroup E] [MulActionWithZero 𝕜 E]
[TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : IsOpen s) (h's : s.Nonempty) :
#s = #E := by
rcases h's with ⟨x, hx⟩
exact cardinal_eq_of_mem_nhds 𝕜 (hs.mem_nhds hx)
