Theorem FirstOrder.Language.Sentence.realize_top

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.realize_topView on Github →