lift_cardinalMk_adjoin_le — Mathlib

English

A bound for the cardinality of adjoin in terms of F, s and an aleph-null, showing lift preserves order up to a maximum.

Русский

Граница кардинала для адъюнкта в терминах F, множества s и алеп-нулевого; отображение сохраняет порядок до максимума.

LaTeX

$$Cardinal.lift #(adjoin F s) ≤ Cardinallift F ⊔ Cardinallift s ⊔ ℵ₀$$

Lean4

theorem lift_cardinalMk_adjoin_le {E : Type v} [Field E] [Algebra F E] (s : Set E) :
    Cardinal.lift.{u} #(adjoin F s) ≤ Cardinal.lift.{v} #F ⊔ Cardinal.lift.{u} #s ⊔ ℵ₀ :=
  by
  rw [show ↥(adjoin F s) = (adjoin F s).toSubfield from rfl, adjoin_toSubfield]
  apply (Cardinal.lift_le.mpr (Subfield.cardinalMk_closure_le_max _)).trans
  rw [lift_max, sup_le_iff, lift_aleph0]
  refine ⟨(Cardinal.lift_le.mpr ((mk_union_le _ _).trans <| add_le_max _ _)).trans ?_, le_sup_right⟩
  simp_rw [lift_max, lift_aleph0]
  grw [mk_range_le_lift]

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