imp_iff_not_sup

Mathlib.ModelTheory.Equivalence

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

English

The implication φ → ψ is equivalent to ¬φ ∨ ψ, modulo T.

Русский

Импликация φ → ψ эквивалентна ¬φ ∨ ψ по отношению к T.

LaTeX

$$$$ (\varphi \Rightarrow_T \psi) \iff_T \neg \varphi \lor \psi $$$$

Lean4

theorem imp_iff_not_sup : (φ.imp ψ) ⇔[T] (φ.not ⊔ ψ) := fun M v xs => by simp [imp_iff_not_or]

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

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

Разделы

Аффилиация

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