English
For any neighborhood of a point x in a topological vector space over a nontrivially normed field, #s = #E.
Русский
Для любой окрестности точки x в топологическом векторном пространства над ненулевым нормированным полем выполняется #s = #E.
LaTeX
$$$#s = #E$ for any $s$ with $s\\in 𝓝 x$.$$
Lean4
/-- In a topological vector space over a nontrivially normed field, any neighborhood of a point has
the same cardinality as the whole space. -/
theorem cardinal_eq_of_mem_nhds {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [AddGroup E] [MulActionWithZero 𝕜 E]
[TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {s : Set E} {x : E} (hs : s ∈ 𝓝 x) : #s = #E :=
by
let g := Homeomorph.addLeft x
let t := g ⁻¹' s
have : t ∈ 𝓝 0 := g.continuous.continuousAt.preimage_mem_nhds (by simpa [g] using hs)
have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this
have B : #t = #s := Cardinal.mk_subtype_of_equiv s g.toEquiv
rwa [B] at A
