Commit 2022-05-27 17:41 1ccb7f04

View on Github →

feat(model_theory/syntax, semantics): Lemmas about relabeling variables (#14225) Proves lemmas about relabeling variables in terms and formulas Defines first_order.language.bounded_formula.to_formula, which turns turns all of the extra variables of a bounded_formula into free variables.

Estimated changes

Modified src/logic/equiv/fin.lean

added theorem fin_sum_fin_equiv_symm_last

Modified src/model_theory/semantics.lean

added theorem first_order.language.bounded_formula.realize_to_formula

Modified src/model_theory/syntax.lean

modified def first_order.language.bounded_formula.cast_le

modified def first_order.language.bounded_formula.relabel

modified def first_order.language.bounded_formula.relabel_aux

added theorem first_order.language.bounded_formula.relabel_aux_sum_inl

added theorem first_order.language.bounded_formula.relabel_sum_inl

added def first_order.language.bounded_formula.to_formula

added theorem first_order.language.term.relabel_id

added theorem first_order.language.term.relabel_relabel