Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 22:40 32e5b6b9

View on Github →

feat(model_theory/terms_and_formulas): Casting and lifting terms and formulas (#12467) Defines bounded_formula.cast_le, which maps the fin-indexed variables with fin.cast_le Defines term.lift_at and bounded_formula.lift_at, which raise fin-indexed variables above a certain threshold

Estimated changes

Modified src/data/fin/basic.lean

added theorem fin.add_nat_one

added theorem fin.cast_cast_succ

added theorem fin.cast_last

added theorem fin.cast_le_of_eq

added theorem fin.cast_zero

Modified src/data/sum/basic.lean

added theorem sum.elim_comp_map

Modified src/model_theory/terms_and_formulas.lean

added def first_order.language.bounded_formula.cast_le

added def first_order.language.bounded_formula.lift_at

added theorem first_order.language.bounded_formula.realize_all_lift_at_one_self

added theorem first_order.language.bounded_formula.realize_cast_le_of_eq

added theorem first_order.language.bounded_formula.realize_lift_at

added theorem first_order.language.bounded_formula.realize_lift_at_one

added theorem first_order.language.bounded_formula.realize_lift_at_one_self

added theorem first_order.language.bounded_formula.semantically_equivalent_all_lift_at

added def first_order.language.term.lift_at

added theorem first_order.language.term.realize_lift_at