equivSentence_not

Mathlib.ModelTheory.Syntax

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

English

Mapping not-preserving formulas to sentences via equivSentence preserves logical negation.

Русский

Перенос логического отрицания через эквивалентность сохраняется при преобразовании equivSentence.

LaTeX

$$$equivSentence\\_not(\\varphi) = (equivSentence(\\varphi)).not$$$

Lean4

theorem equivSentence_not (φ : L.Formula α) : equivSentence φ.not = (equivSentence φ).not :=
  rfl

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

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

Разделы

Аффилиация

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