imp_iff_not_sup

Mathlib.ModelTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Formula.imp_iff_not_sup

English

In a theory T, φ → ψ is equivalent to ¬φ ∨ ψ.

Русский

В теории T φ → ψ эквивалентно ¬φ ∨ ψ.

LaTeX

$$$T \models (\varphi \rightarrow \psi) \leftrightarrow (\lnot \varphi \lor \psi)$$$

Lean4

theorem imp_iff_not_sup : (φ.imp ψ) ⇔[T] (φ.not ⊔ ψ) :=
  BoundedFormula.imp_iff_not_sup φ ψ

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru