sup_iff_not_inf_not

Mathlib.ModelTheory.Equivalence

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

English

In a theory T, φ ∨ ψ is equivalent to ¬(¬φ ∧ ¬ψ).

Русский

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

LaTeX

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

Lean4

theorem sup_iff_not_inf_not : (φ ⊔ ψ) ⇔[T] (φ.not ⊓ ψ.not).not :=
  BoundedFormula.sup_iff_not_inf_not φ ψ

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

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

Разделы

Аффилиация

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