Theorem FirstOrder.Language.empty.isFraisse_finite

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.isFraisse_finiteView on Github →