ex_iff_not_all_not

Mathlib.ModelTheory.Equivalence

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

English

There exists a witness for φ is equivalent to not of all not for φ.

Русский

Существование свидетеля для φ эквивалентно несуществованию всех не для φ.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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