iff_not_not

Mathlib.ModelTheory.Equivalence

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

English

If φ ⇔ ψ, then in any model M, φ and ψ have the same truth value.

Русский

Если φ эквивалентно ψ, то в любой модели M они имеют одинаковую истинность.

LaTeX

$$$$ M \vDash \varphi \iff M \vDash \psi $$$$

Lean4

theorem iff_not_not : φ ⇔[T] φ.not.not := fun M v xs => by simp

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

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

Разделы

Аффилиация

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