lift_card_closure_le — Mathlib

English

The cardinality of the closure is bounded by the maximum of aleph-null and the sum of the cardinalities of s and the set of all function symbols.

Русский

Кардинал замыкания ограничен максимумом слева по мастеру: aleph-null и сумма кардиналов s и множества всех символьных функций.

LaTeX

$$$$ \operatorname{lift} \#(\operatorname{closure}_L(s)) \le \max\left( \aleph_0, \operatorname{lift}\#s + \operatorname{lift}\#\left(\sum_i L.\mathrm{Functions}(i)\right) \right). $$$$

Lean4

theorem lift_card_closure_le :
    Cardinal.lift.{u, w} #(closure L s) ≤
      max ℵ₀ (Cardinal.lift.{u, w} #s + Cardinal.lift.{w, u} #(Σ i, L.Functions i)) :=
  by
  rw [← lift_umax]
  refine lift_card_closure_le_card_term.trans (Term.card_le.trans ?_)
  rw [mk_sum, lift_umax.{w, u}]

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