card_functions_sum_skolem₁_le — Mathlib

English

The total number of Skolem-augmented function symbols is bounded by the maximum of aleph0 and the language size.

Русский

Для любого L кардинальность суммы по n от (L.sum L.skolem₁).Functions n не превосходит max(ℵ0, card(L)).

LaTeX

$$Cardinal.instLE.le (Cardinal.mk ((Σ n) (L.sum L.skolem₁).Functions n)) (SemilatticeSup.toMax.max Cardinal.aleph0 L.card)$$

Lean4

theorem card_functions_sum_skolem₁_le : #(Σ n, (L.sum L.skolem₁).Functions n) ≤ max ℵ₀ L.card :=
  by
  rw [card_functions_sum_skolem₁]
  trans #(Σ n, L.BoundedFormula Empty n)
  · exact ⟨⟨Sigma.map Nat.succ fun _ => id, Nat.succ_injective.sigma_map fun _ => Function.injective_id⟩⟩
  · refine _root_.trans BoundedFormula.card_le (lift_le.{max u v}.1 ?_)
    simp only [mk_empty, lift_zero, lift_uzero, zero_add]
    rfl

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