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.ModelsBoundedFormula.realize_formula