substructure_closure — Mathlib

English

If s is countable (and the signature is countable), then the closure of s is countable.

Русский

Если s счётно, и сигнатура счётна, тогда замыкание s по L счётно.

LaTeX

$$$$ s \text{Countable} \Rightarrow \operatorname{Countable}(\operatorname{closure}_L(s)). $$$$

Lean4

theorem _root_.Set.Countable.substructure_closure [Countable (Σ l, L.Functions l)] (h : s.Countable) :
    Countable.{w + 1} (closure L s) := by
  haveI : Countable s := h.to_subtype
  rw [← mk_le_aleph0_iff, ← lift_le_aleph0]
  exact lift_card_closure_le_card_term.trans mk_le_aleph0

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