Commit 2024-04-06 15:25 0d98b682

View on Github →

feat(ModelTheory): lift of equivalences between direct limits, and direct limit of system of substructures (#11174) Define the equivalence between direct limits of isomorphic systems, and the equivalence between the direct limit of a system of substructures and the union of these substructures.

Estimated changes

Modified Mathlib/ModelTheory/Basic.lean

added theorem FirstOrder.Language.Embedding.toHom_inj

added theorem FirstOrder.Language.Embedding.toHom_injective

Modified Mathlib/ModelTheory/DirectLimit.lean

added theorem FirstOrder.Language.DirectLimit.Equiv_isup_of_apply

added theorem FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion

added theorem FirstOrder.Language.DirectLimit.Equiv_isup_symm_inclusion_apply

added theorem FirstOrder.Language.DirectLimit.equiv_lift_of

added theorem FirstOrder.Language.DirectLimit.exists_fg_substructure_in_Sigma

added theorem FirstOrder.Language.DirectLimit.iSup_range_of_eq_top

added def FirstOrder.Language.DirectLimit.liftInclusion

added theorem FirstOrder.Language.DirectLimit.liftInclusion_of

added theorem FirstOrder.Language.DirectLimit.rangeLiftInclusion

added theorem FirstOrder.Language.DirectLimit.range_lift

Modified Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.Embedding.codRestrict_apply'

added theorem FirstOrder.Language.Embedding.subtype_equivRange

added theorem FirstOrder.Language.Embedding.subtype_substructureEquivMap

added theorem FirstOrder.Language.Substructure.inclusion_self