continuum_le_cardinal_of_module — Mathlib

English

A nontrivial module E over a complete nontrivially normed field 𝕜 satisfies 𝔠 ≤ #E.

Русский

Не-тривиальный модуль E над полем 𝕜 с полным нормированием удовлетворяет 𝔠 ≤ |E|.

LaTeX

$$$\\mathfrak{c} \\le |E|$$$

Lean4

/-- A nontrivial module over a complete nontrivially normed field has cardinality at least
continuum. -/
theorem continuum_le_cardinal_of_module (𝕜 : Type u) (E : Type v) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [Nontrivial E] : 𝔠 ≤ #E :=
  by
  have A : lift.{v} (𝔠 : Cardinal.{u}) ≤ lift.{v} (#𝕜) := by
    simpa using continuum_le_cardinal_of_nontriviallyNormedField 𝕜
  simpa using A.trans (Cardinal.mk_le_of_module 𝕜 E)

Похожие утверждения