Theorem FirstOrder.Language.BoundedFormula.realize_restrictFreeVar'

Modification history

2024-12-23 10:59

Mathlib/ModelTheory/Semantics.lean

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

Added FirstOrder.Language.BoundedFormula.realize_restrictFreeVar'View on Github →