Commit 2024-08-14 14:06 f494f96e

View on Github →

feat(ModelTheory/FinitelyGenerated): only countably many morphisms from a cg structure to a countable one (#11177) Prove that there are only countably many morphisms from a countably generated structure, to a countable one.

Estimated changes

Modified Mathlib/ModelTheory/FinitelyGenerated.lean

added theorem FirstOrder.Language.Structure.FG.countable_embedding

added theorem FirstOrder.Language.Structure.FG.countable_hom

added theorem FirstOrder.Language.Structure.cg_of_countable

added theorem FirstOrder.Language.Substructure.cg_of_countable

added theorem FirstOrder.Language.Substructure.countable_fg_substructures_of_countable

Modified Mathlib/ModelTheory/PartialEquiv.lean

added theorem FirstOrder.Language.DirectLimit.cod_partialEquivLimit

added theorem FirstOrder.Language.DirectLimit.dom_partialEquivLimit

added theorem FirstOrder.Language.DirectLimit.le_partialEquivLimit

added theorem FirstOrder.Language.DirectLimit.partialEquivLimit_comp_inclusion

added def FirstOrder.Language.FGEquiv.symm

added def FirstOrder.Language.IsExtensionPair.definedAtLeft

added def FirstOrder.Language.IsExtensionPair.definedAtRight

added def FirstOrder.Language.IsExtensionPair

added theorem FirstOrder.Language.IsExtensionPair_iff_cod

added theorem FirstOrder.Language.PartialEquiv.dom_fg_iff_cod_fg

added theorem FirstOrder.Language.countable_self_fgequiv_of_countable

added theorem FirstOrder.Language.embedding_from_cg

added theorem FirstOrder.Language.equiv_between_cg

Modified Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.Substructure.subtype_comp_inclusion