cardinalMk_le_mul — Mathlib

English

The cardinality of the set of algebraic elements is bounded by the product of the cardinality of R[X] and aleph-null.

Русский

Кардинальность множества алгебраических элементов ограничена произведением кардинальности R[X] и aleph-null.

LaTeX

$$$\#\{ x \in A \mid IsAlgebraic(R, x) \} \le |R[X]| \cdot \aleph_0$$$

Lean4

theorem cardinalMk_le_mul : #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀ :=
  by
  rw [← lift_id #_, ← lift_id #R[X]]
  exact cardinalMk_lift_le_mul R A

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