Commit 2023-07-04 18:38 d57f6f35

View on Github →

feat: port ModelTheory.DirectLimit (#4391)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/DirectLimit.lean

added theorem FirstOrder.Language.DirectLimit.cG

added theorem FirstOrder.Language.DirectLimit.comp_unify

added theorem FirstOrder.Language.DirectLimit.equiv_iff

added theorem FirstOrder.Language.DirectLimit.exists_of

added theorem FirstOrder.Language.DirectLimit.exists_quotient_mk'_sigma_mk'_eq

added theorem FirstOrder.Language.DirectLimit.exists_unify_eq

added theorem FirstOrder.Language.DirectLimit.funMap_equiv_unify

added theorem FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk'

added theorem FirstOrder.Language.DirectLimit.funMap_unify_equiv

added def FirstOrder.Language.DirectLimit.lift

added theorem FirstOrder.Language.DirectLimit.lift_of

added theorem FirstOrder.Language.DirectLimit.lift_quotient_mk'_sigma_mk'

added theorem FirstOrder.Language.DirectLimit.lift_unique

added def FirstOrder.Language.DirectLimit.of

added theorem FirstOrder.Language.DirectLimit.of_apply

added theorem FirstOrder.Language.DirectLimit.of_f

added theorem FirstOrder.Language.DirectLimit.relMap_equiv_unify

added theorem FirstOrder.Language.DirectLimit.relMap_quotient_mk'_sigma_mk'

added theorem FirstOrder.Language.DirectLimit.relMap_unify_equiv

added def FirstOrder.Language.DirectLimit.setoid

added def FirstOrder.Language.DirectLimit.unify

added theorem FirstOrder.Language.DirectLimit.unify_sigma_mk_self

added def FirstOrder.Language.DirectLimit

added theorem FirstOrder.Language.DirectedSystem.coe_natLeRec

added def FirstOrder.Language.DirectedSystem.natLeRec