inf_not_iff_bot — Mathlib

English

Let φ be any formula in a theory T. Then φ ∧ ¬φ is equivalent to ⊥ (i.e., false) under T.

Русский

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

LaTeX

$$$T \models (\varphi \land \lnot \varphi) \leftrightarrow \bot$$$

Lean4

theorem inf_not_iff_bot : φ ⊓ ∼φ ⇔[T] ⊥ := fun M v xs => by
  simp only [realize_iff, realize_inf, realize_not, and_not_self, realize_bot]

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