Complement closure for isomorphism-invariant classes #
The complement of an isomorphism-invariant class of coded structures is again invariant. This elementary lemma is the only closure property needed by the retained López–Escobar branch.
theorem
FirstOrder.Language.IsomorphismInvariant.compl
{L : Language}
[L.IsRelational]
{B : Set L.StructureSpace}
(h : IsomorphismInvariant B)
:
Isomorphism invariance is closed under complement.