Theorem FirstOrder.Language.Sentence.not_realize_bot

Modification history

2026-06-04 02:30

Mathlib/ModelTheory/Semantics.lean

feat(ModelTheory/Semantics): add simp theorems similar to Sentence.realize_not (#39996) …

Added FirstOrder.Language.Sentence.not_realize_bot View on Github →