Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-22 20:22 3838b852

View on Github →

feat(model_theory/*): Language equivalences (#12837) Defines equivalences between first-order languages

Estimated changes

Modified src/model_theory/basic.lean

added def first_order.language.Lequiv.add_empty_constants

added structure first_order.language.Lequiv

modified def first_order.language.Lhom.comp

added theorem first_order.language.Lhom.comp_assoc

modified theorem first_order.language.Lhom.comp_id

added theorem first_order.language.Lhom.comp_sum_elim

modified theorem first_order.language.Lhom.id_comp

added theorem first_order.language.Lhom.map_constants_comp_sum_inl

deleted theorem first_order.language.Lhom.map_constants_comp_with_constants

deleted def first_order.language.Lhom.sum_elim

added theorem first_order.language.Lhom.sum_elim_comp_inl

added theorem first_order.language.Lhom.sum_elim_comp_inr

added theorem first_order.language.Lhom.sum_elim_inl_inr

modified def first_order.language.Lhom.sum_map

added theorem first_order.language.Lhom.sum_map_comp_inl

added theorem first_order.language.Lhom.sum_map_comp_inr

deleted def first_order.language.Lhom_trim_empty_constants

modified def first_order.language.Lhom_with_constants

Modified src/model_theory/definability.lean

Modified src/model_theory/terms_and_formulas.lean

added def first_order.language.Lequiv.on_bounded_formula

added theorem first_order.language.Lequiv.on_bounded_formula_symm

added def first_order.language.Lequiv.on_formula

added theorem first_order.language.Lequiv.on_formula_apply

added theorem first_order.language.Lequiv.on_formula_symm

added def first_order.language.Lequiv.on_sentence

added def first_order.language.Lequiv.on_term

added theorem first_order.language.Lhom.comp_on_bounded_formula

added theorem first_order.language.Lhom.comp_on_term

added theorem first_order.language.Lhom.id_on_bounded_formula

added theorem first_order.language.Lhom.id_on_term

modified def first_order.language.Lhom.on_bounded_formula

modified def first_order.language.Lhom.on_formula

modified def first_order.language.Lhom.on_term

modified theorem first_order.language.Lhom.realize_on_term

added theorem first_order.language.Lhom.set_of_realize_on_formula