Theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not

Modification history

2024-09-17 09:07

Mathlib/ModelTheory/Equivalence.lean

chore(ModelTheory/Equivalence): Cleanup of `FirstOrder.Language.Theory.SemanticallyEquivalent` (#16799) …

Modified FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not View on Github →

2023-05-25 08:25

Mathlib/ModelTheory/Satisfiability.lean

feat: port ModelTheory.Satisfiability (#3980)

Added FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not View on Github →