mathlib3
32e5b6b9 - feat(model_theory/terms_and_formulas): Casting and lifting terms and formulas (#12467)

Commit
3 years ago
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 Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
Author
Parents
Loading