not

Mathlib.ModelTheory.Equivalence

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Theory.Iff.not

← MathLib Explorer

English

From φ ⇔ ψ, derive φ.not ⇔ ψ.not.

Русский

Из φ ⇔ ψ следует φ.not ⇔ ψ.not.

LaTeX

$$$$ (\varphi \iff_T \psi) \Rightarrow (\varphi.not \iff_T \psi.not) $$$$

Lean4

protected theorem not {φ ψ : L.BoundedFormula α n} (h : φ ⇔[T] ψ) : φ.not ⇔[T] ψ.not :=
  by
  simp_rw [Theory.Iff, ModelsBoundedFormula, BoundedFormula.realize_iff, BoundedFormula.realize_not]
  exact fun M v xs => not_congr h.realize_bd_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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