Commit 2023-05-13 13:28 e53458ae

View on Github →

feat: port ModelTheory.FinitelyGenerated (#3927)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/FinitelyGenerated.lean

added theorem FirstOrder.Language.Equiv.cg_iff

added theorem FirstOrder.Language.Equiv.fg_iff

added theorem FirstOrder.Language.Structure.CG.map_of_surjective

added theorem FirstOrder.Language.Structure.CG.range

added theorem FirstOrder.Language.Structure.FG.cg

added theorem FirstOrder.Language.Structure.FG.map_of_surjective

added theorem FirstOrder.Language.Structure.FG.range

added theorem FirstOrder.Language.Structure.cg_def

added theorem FirstOrder.Language.Structure.cg_iff

added theorem FirstOrder.Language.Structure.cg_iff_countable

added theorem FirstOrder.Language.Structure.fg_def

added theorem FirstOrder.Language.Structure.fg_iff

added theorem FirstOrder.Language.Substructure.CG.map

added theorem FirstOrder.Language.Substructure.CG.of_map_embedding

added theorem FirstOrder.Language.Substructure.CG.sup

added def FirstOrder.Language.Substructure.CG

added theorem FirstOrder.Language.Substructure.FG.cg

added theorem FirstOrder.Language.Substructure.FG.map

added theorem FirstOrder.Language.Substructure.FG.of_map_embedding

added theorem FirstOrder.Language.Substructure.FG.sup

added def FirstOrder.Language.Substructure.FG

added theorem FirstOrder.Language.Substructure.cg_bot

added theorem FirstOrder.Language.Substructure.cg_closure

added theorem FirstOrder.Language.Substructure.cg_closure_singleton

added theorem FirstOrder.Language.Substructure.cg_def

added theorem FirstOrder.Language.Substructure.cg_iff_countable

added theorem FirstOrder.Language.Substructure.cg_iff_empty_or_exists_nat_generating_family

added theorem FirstOrder.Language.Substructure.cg_iff_structure_cg

added theorem FirstOrder.Language.Substructure.fg_bot

added theorem FirstOrder.Language.Substructure.fg_closure

added theorem FirstOrder.Language.Substructure.fg_closure_singleton

added theorem FirstOrder.Language.Substructure.fg_def

added theorem FirstOrder.Language.Substructure.fg_iff_exists_fin_generating_family

added theorem FirstOrder.Language.Substructure.fg_iff_structure_fg