Theorem FirstOrder.Language.empty.isFraisseLimit_of_countable_infinite

Modification history

2024-09-04 09:43
Mathlib/ModelTheory/Fraisse.lean
feat(ModelTheory/Fraisse): Shows that any countably infinite structure in the empty language is a Fraïssé limit (#16194) …
Added FirstOrder.Language.empty.isFraisseLimit_of_countable_infiniteView on Github →