Theorem FirstOrder.Language.Term.realize_restrictVar

Modification history

2024-12-23 10:59

Mathlib/ModelTheory/Semantics.lean

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

Modified FirstOrder.Language.Term.realize_restrictVar View on Github →

2023-05-12 15:18

Mathlib/ModelTheory/Semantics.lean

feat: port ModelTheory.Semantics (#3196)

Added FirstOrder.Language.Term.realize_restrictVar View on Github →