Commit 2022-06-15 11:13 c6677234

View on Github →

feat(model_theory/syntax, semantics): Mapping formulas given maps on terms and relations (#14466) Defines first_order.language.bounded_formula.map_term_rel, which maps formulas given maps on terms and maps on relations.

Estimated changes

Modified src/data/fin/basic.lean

added theorem fin.cast_le_cast_le

added theorem fin.cast_le_comp_cast_le

added theorem fin.nat_add_cast_succ

added theorem fin.nat_add_last

Modified src/data/fin/tuple/basic.lean

added theorem fin.snoc_cast_add

added theorem fin.snoc_comp_cast_add

added theorem fin.snoc_comp_nat_add

Modified src/model_theory/semantics.lean

added theorem first_order.language.bounded_formula.realize_map_term_rel_add_cast_le

added theorem first_order.language.bounded_formula.realize_map_term_rel_id

deleted theorem first_order.language.bounded_formula.realize_subst_aux

Modified src/model_theory/syntax.lean

added theorem first_order.language.bounded_formula.cast_le_cast_le

added theorem first_order.language.bounded_formula.cast_le_comp_cast_le

added theorem first_order.language.bounded_formula.cast_le_rfl

modified def first_order.language.bounded_formula.lift_at

added def first_order.language.bounded_formula.map_term_rel

added def first_order.language.bounded_formula.map_term_rel_equiv

added theorem first_order.language.bounded_formula.map_term_rel_id_id_id

added theorem first_order.language.bounded_formula.map_term_rel_map_term_rel

modified def first_order.language.bounded_formula.relabel

added theorem first_order.language.bounded_formula.relabel_all

added theorem first_order.language.bounded_formula.relabel_bot

added theorem first_order.language.bounded_formula.relabel_ex

added theorem first_order.language.bounded_formula.relabel_falsum

added theorem first_order.language.bounded_formula.relabel_imp

added theorem first_order.language.bounded_formula.relabel_not

modified def first_order.language.bounded_formula.subst

added theorem first_order.language.term.relabel_comp_relabel

modified theorem first_order.language.term.relabel_id

added theorem first_order.language.term.relabel_id_eq_id