FirstOrder.Language.Term.card_le

theorem FirstOrder.Language.Term.card_le : ∀ {L : FirstOrder.Language} {α : Type u'}, Cardinal.mk (L.Term α) ≤ max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))

This theorem states that for any first-order language `L` and any type `α`, the cardinality of the set of terms of `L` with variables from `α` is less than or equal to the maximum of `ℵ₀` (the smallest infinite cardinal number) and the cardinality of the disjoint union of `α` and the set of all functions from `ℵ₀` (the set of natural numbers) to the functions of `L`. In essence, it provides an upper bound for the size of the set of terms in a given first-order language and variable type, in terms of the language's functions and the variable type's cardinality.

More concisely: For any first-order language L and type α, the number of terms of L with variables from α is below the cardinality of ℵ₀ + |α| + |L|^(|α|).