English
A complete, nontrivially normed field has cardinality at least the continuum.
Русский
Поле полного нормированного поля с ненулевой элементарной структурой имеет кардинальность не меньше континуум.
LaTeX
$$$\\mathfrak{c} \\le |\\mathbb{k}|$$$
Lean4
/-- A complete nontrivially normed field has cardinality at least continuum. -/
theorem continuum_le_cardinal_of_nontriviallyNormedField (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] :
𝔠 ≤ #𝕜 :=
by
suffices ∃ f : (ℕ → Bool) → 𝕜, range f ⊆ univ ∧ Continuous f ∧ Injective f
by
rcases this with ⟨f, -, -, f_inj⟩
simpa using lift_mk_le_lift_mk_of_injective f_inj
apply Perfect.exists_nat_bool_injection _ univ_nonempty
refine ⟨isClosed_univ, preperfect_iff_nhds.2 (fun x _ U hU ↦ ?_)⟩
rcases NormedField.exists_norm_lt_one 𝕜 with ⟨c, c_pos, hc⟩
have A : Tendsto (fun n ↦ x + c ^ n) atTop (𝓝 (x + 0)) :=
tendsto_const_nhds.add (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc)
rw [add_zero] at A
have B : ∀ᶠ n in atTop, x + c ^ n ∈ U := tendsto_def.1 A U hU
rcases B.exists with ⟨n, hn⟩
refine ⟨x + c ^ n, by simpa using hn, ?_⟩
simp only [add_ne_left]
apply pow_ne_zero
simpa using c_pos
