all_iff_not_ex_not

Mathlib.ModelTheory.Equivalence

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

English

For any φ, φ.all is equivalent to φ.not.ex.not.

Русский

Для любой φ, φ.all эквивалентно φ.not.ex.not.

LaTeX

$$$$ \varphi.all \iff_T \varphi.not.ex.not $$$$

Lean4

theorem all_iff_not_ex_not (φ : L.BoundedFormula α (n + 1)) : φ.all ⇔[T] φ.not.ex.not := fun M v xs => by simp

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

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

Разделы

Аффилиация

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