Commit 2024-08-27 20:26 fa7fd3cb

View on Github →

chore(ModelTheory): Tweaks involving the empty language (#16192) Makes FirstOrder.Language.emptyStructure a def instead of an instance Removes defs that could be accomplished with StrongHomClass.toEmbedding and StrongHomClass.toEquiv

Estimated changes

Modified Mathlib/ModelTheory/Basic.lean

deleted def Embedding.empty

deleted def Equiv.empty

added def FirstOrder.Language.emptyStructure

deleted theorem FirstOrder.Language.toEmbedding_embedding_empty

deleted theorem FirstOrder.Language.toEquiv_equiv_empty

deleted theorem FirstOrder.Language.toFun_embedding_empty

deleted theorem FirstOrder.Language.toFun_equiv_empty

Modified Mathlib/ModelTheory/Satisfiability.lean