Cardinality of generated substructures

Mathlib's FirstOrder.Language.Substructure.lift_card_closure_le bounds the substructure generated by a set s by max ℵ₀ (|s| + |Σ n, L.Functions n|). This file restates it in the common universe of the language and the structure, as a bound by any infinite cardinal that bounds both s and the function symbols.

Main results

• FirstOrder.Language.Substructure.lift_mk_closure_le: the substructure generated by at most κ elements has at most κ elements, for an infinite κ bounding the function symbols.

theorem FirstOrder.Language.Substructure.lift_mk_closure_le {L : Language} {M : Type w} [L.Structure M] {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hF : Cardinal.lift.{max v w, u} (Cardinal.mk ((n : ℕ) × L.Functions n)) ≤ κ) {s : Set M} (hs : Cardinal.lift.{max u v, w} (Cardinal.mk ↑s) ≤ κ) : Cardinal.lift.{max u v, w} (Cardinal.mk ↥((closure L).toFun s)) ≤ κ

The closure of at most κ elements has at most κ elements, for an infinite cardinal κ in the common universe max u v w that bounds the set and the function symbols.