English
A bound on the cardinality of the set of all bounded formulas over a language is given by a specific max of aleph-null and lifts of α and the language's card.
Русский
Задан предел кардинальности множества ограниченных формул над языком: максимум ℵ0 и соответствующие подстановки α и кардинал языка.
LaTeX
$$$#((\\Sigma n, L.BoundedFormula α n)) \\leq \\max(\\aleph_0, \\operatorname{lift}^{{\\max u v}} #α + \\operatorname{lift}^{u'} L.card)$$$
Lean4
theorem card_le : #(Σ n, L.BoundedFormula α n) ≤ max ℵ₀ (Cardinal.lift.{max u v} #α + Cardinal.lift.{u'} L.card) :=
by
refine lift_le.1 (BoundedFormula.encoding.card_le_card_list.trans ?_)
rw [encoding_Γ, mk_list_eq_max_mk_aleph0, lift_max, lift_aleph0, lift_max, lift_aleph0, max_le_iff]
refine ⟨?_, le_max_left _ _⟩
rw [mk_sum, Term.card_sigma, mk_sum, ← add_eq_max le_rfl, mk_sum, mk_nat]
simp only [lift_add, lift_lift, lift_aleph0]
rw [← add_assoc, add_comm, ← add_assoc, ← add_assoc, aleph0_add_aleph0, add_assoc, add_eq_max le_rfl, add_assoc, card,
Symbols, mk_sum, lift_add, lift_lift, lift_lift]
