English
In a topological vector space over a nontrivially normed field, any neighborhood of zero has the same cardinality as the whole space.
Русский
В топологическом векторном пространстве над ненулевым нормированным полем любое окрестное множество нуля имеет ту же кардинальность, что и всё пространство.
LaTeX
$$$#s = #E$ whenever $0 \\in s$ and $s$ is a neighborhood of $0$.$$
Lean4
/-- 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`. -/
theorem cardinal_eq_of_mem_nhds_zero {E : Type*} (𝕜 : Type*) [NontriviallyNormedField 𝕜] [Zero E]
[MulActionWithZero 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s ∈ 𝓝 (0 : E)) : #s = #E := by
/- As `s` is a neighborhood of `0`, the space is covered by the rescaled sets `c^n • s`,
where `c` is any element of `𝕜` with norm `> 1`. All these sets are in bijection and have
therefore the same cardinality. The conclusion follows. -/
obtain ⟨c, hc⟩ : ∃ x : 𝕜, 1 < ‖x‖ := NormedField.exists_lt_norm 𝕜 1
have cn_ne : ∀ n, c ^ n ≠ 0 := by
intro n
apply pow_ne_zero
rintro rfl
simp only [norm_zero] at hc
exact lt_irrefl _ (hc.trans zero_lt_one)
have A : ∀ (x : E), ∀ᶠ n in (atTop : Filter ℕ), x ∈ c ^ n • s :=
by
intro x
have : Tendsto (fun n ↦ (c ^ n)⁻¹ • x) atTop (𝓝 ((0 : 𝕜) • x)) :=
by
have : Tendsto (fun n ↦ (c ^ n)⁻¹) atTop (𝓝 0) :=
by
simp_rw [← inv_pow]
apply tendsto_pow_atTop_nhds_zero_of_norm_lt_one
rw [norm_inv]
exact inv_lt_one_of_one_lt₀ hc
exact Tendsto.smul_const this x
rw [zero_smul] at this
filter_upwards [this hs] with n (hn : (c ^ n)⁻¹ • x ∈ s)
exact (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).2 hn
have B : ∀ n, #(c ^ n • s :) = #s := by
intro n
have : (c ^ n • s :) ≃ s :=
{ toFun := fun x ↦ ⟨(c ^ n)⁻¹ • x.1, (mem_smul_set_iff_inv_smul_mem₀ (cn_ne n) _ _).1 x.2⟩
invFun := fun x ↦ ⟨(c ^ n) • x.1, smul_mem_smul_set x.2⟩
left_inv := fun x ↦ by simp [smul_smul, mul_inv_cancel₀ (cn_ne n)]
right_inv := fun x ↦ by simp [smul_smul, inv_mul_cancel₀ (cn_ne n)] }
exact Cardinal.mk_congr this
apply (Cardinal.mk_of_countable_eventually_mem A B).symm
