Commit 2024-12-23 10:59 49dfbf20

View on Github →

chore(ModelTheory): restate some theorems about restricting variables (#20115)

Estimated changes

Modified Mathlib/ModelTheory/Definability.lean

Modified Mathlib/ModelTheory/ElementaryMaps.lean

Modified Mathlib/ModelTheory/Semantics.lean

added theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar'

modified theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar

added theorem FirstOrder.Language.Term.realize_restrictVar'

modified theorem FirstOrder.Language.Term.realize_restrictVar

added theorem FirstOrder.Language.Term.realize_restrictVarLeft'

modified theorem FirstOrder.Language.Term.realize_restrictVarLeft