English
For a nontrivially normed field 𝕜 and a nontrivial complete space, every nonempty open set has size at least continuum.
Русский
Для ненулевого нормированного поля 𝕜 и непустого открытого пространства вытекает: размер любого непустого открытого множества не меньше континуум.
LaTeX
$$$IsOpen s \\Rightarrow s \\neq \\emptyset \\Rightarrow 𝔠 \\le #s$.$$
Lean4
/-- In a nontrivial topological vector space over a complete nontrivially normed field, any nonempty
open set has cardinality at least continuum. -/
theorem continuum_le_cardinal_of_isOpen {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
[AddCommGroup E] [Module 𝕜 E] [Nontrivial E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E}
(hs : IsOpen s) (h's : s.Nonempty) : 𝔠 ≤ #s := by
simpa [cardinal_eq_of_isOpen 𝕜 hs h's] using continuum_le_cardinal_of_module 𝕜 E
