lift_cardinalMk_adjoin_le — Mathlib

English

For any A with R-algebra structure and any s ⊆ A, the cardinality of adjoin R s is bounded by lift(#R) ⊔ lift(#s) ⊔ ℵ0.

Русский

Для любой A с структурой R-алгебры и подмножества s ⊆ A кардинал аджойна ограничен верхом lift(#R) ⊔ lift(#s) ⊔ ℵ0.

LaTeX

$$lift.{u} #(adjoin R s) ≤ lift.{v} #R ⊔ lift.{u} #s ⊔ ℵ₀$$

Lean4

theorem lift_cardinalMk_adjoin_le {A : Type v} [Semiring A] [Algebra R A] (s : Set A) :
    lift.{u} #(adjoin R s) ≤ lift.{v} #R ⊔ lift.{u} #s ⊔ ℵ₀ :=
  by
  have H := mk_range_le_lift (f := FreeAlgebra.lift R ((↑) : s → A))
  rw [lift_umax, lift_id'.{v, u}] at H
  rw [Algebra.adjoin_eq_range_freeAlgebra_lift]
  exact H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

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