sup_not_iff_top — Mathlib

English

Let φ be any formula in a theory T. Then φ ∨ ¬φ is equivalent to ⊤ (i.e., true) under T.

Русский

Пусть φ — любая формула теории T. Тогда φ ∨ ¬φ тождественно равно ⊤ относительно T.

LaTeX

$$$T \models (\varphi \lor \lnot \varphi) \leftrightarrow \top$$$

Lean4

theorem sup_not_iff_top : φ ⊔ ∼φ ⇔[T] ⊤ := fun M v xs => by
  simp only [realize_iff, realize_sup, realize_not, realize_top, or_not]

Похожие утверждения