Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.countable.substructure_closure

Modification history

2022-09-14 16:17
src/model_theory/substructures.lean
refactor(model_theory/*): Use `countable` in model theory (#16496) …
Modified set.countable.substructure_closureView on Github →
2022-03-24 10:12
src/model_theory/substructures.lean
feat(model_theory/*): Facts about countability of first-order structures (#12819) …
Added set.countable.substructure_closureView on Github →