cardinalMk_le_sigma_polynomial — Mathlib

English

The cardinality of L is bounded by the cardinality of a sigma-polynomial collection, i.e., Lift #L ≤ #(Σ p : R[X], { x ∈ L | x ∈ p.aroots L }).

Русский

Кардинальность L ограничена кардинальностью множества пар (p, x) с p ∈ R[X] и x корень p.

LaTeX

$$$\\operatorname{lift} \\#L \\le \\#\\Bigl(\\Sigma p : R[X], \\{ x : L \\mid x \\in p.aroots(L) \\} \\Bigr)$$$

Lean4

theorem cardinalMk_le_sigma_polynomial : #L ≤ #(Σ p : R[X], { x : L // x ∈ p.aroots L }) := by
  simpa only [lift_id] using lift_cardinalMk_le_sigma_polynomial R L

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