Commit 2022-04-11 09:27 ff507a35

View on Github →

feat(model_theory/basic): Structures over the empty language (#13281) Any type is a first-order structure over the empty language. Any function, embedding, or equiv is a first-order hom, embedding or equiv over the empty language.

Estimated changes

Modified src/model_theory/basic.lean

added def embedding.empty

added def equiv.empty

modified def first_order.language.embedding.to_hom

added theorem first_order.language.empty.nonempty_embedding_iff

added theorem first_order.language.empty.nonempty_equiv_iff

modified def first_order.language.equiv.to_embedding

modified def first_order.language.equiv.to_hom

added def first_order.language.hom_class.to_hom

added def first_order.language.strong_hom_class.to_embedding

added def first_order.language.strong_hom_class.to_equiv

added def function.empty_hom

Modified src/model_theory/language_map.lean

modified def first_order.language.constants_on