Theorem FirstOrder.Language.Theory.models_toFormula_iff

Modification history

2024-09-11 03:54
Mathlib/ModelTheory/Satisfiability.lean
feat(ModelTheory/Satisfiability): Fix universe on ModelsBoundedFormula, derive consequences for models in all universes (#16676) …
Added FirstOrder.Language.Theory.models_toFormula_iffView on Github →