cardinalMk_adjoin_le — Mathlib

English

For an R-algebra A and set s inside A, the cardinality of adjoin R s is at most the max of #R, #s, and ℵ0.

Русский

Для R-алгебры A и множества s внутри A кардинал адъойна не превышает максимум #R, #s и ℵ0.

LaTeX

$$ #(adjoin R s) ≤ #R ⊔ #s ⊔ ℵ₀$$

Lean4

theorem cardinalMk_adjoin_le {A : Type u} [Semiring A] [Algebra R A] (s : Set A) : #(adjoin R s) ≤ #R ⊔ #s ⊔ ℵ₀ := by
  simpa using lift_cardinalMk_adjoin_le R s

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