Commit 2022-08-14 02:18 3baad3bf

View on Github →

feat(model_theory/syntax): Swapping between constants and variables (#14018) term.constants_vars_equiv and bounded_formula.constants_vars_equiv send terms/formulas with constants to terms/formulas with extra variables and back.

Estimated changes

Modified src/model_theory/language_map.lean

added theorem first_order.language.Lhom.fun_map_sum_inl

added theorem first_order.language.Lhom.fun_map_sum_inr

added theorem first_order.language.Lhom.map_on_function

added theorem first_order.language.Lhom.map_on_relation

modified def first_order.language.with_constants

added theorem first_order.language.with_constants_fun_map_sum_inl

added theorem first_order.language.with_constants_fun_map_sum_inr

added theorem first_order.language.with_constants_rel_map_sum_inl

Modified src/model_theory/order.lean

Modified src/model_theory/semantics.lean

added theorem first_order.language.bounded_formula.realize_constants_vars_equiv

added theorem first_order.language.term.realize_constants_to_vars

added theorem first_order.language.term.realize_constants_vars_equiv_left

added theorem first_order.language.term.realize_vars_to_constants

Modified src/model_theory/substructures.lean

Modified src/model_theory/syntax.lean

added def first_order.language.bounded_formula.constants_vars_equiv

added def first_order.language.term.constants_to_vars

added def first_order.language.term.constants_vars_equiv

added def first_order.language.term.constants_vars_equiv_left

added theorem first_order.language.term.constants_vars_equiv_left_apply

added theorem first_order.language.term.constants_vars_equiv_left_symm_apply

added def first_order.language.term.relabel_equiv

added def first_order.language.term.vars_to_constants