rel_not

Mathlib.Logic.Relator

URI: https://scilib.ai/kg/mathlib#Relator.rel_not

English

Negation preserves Iff: if p ↔ q then ¬p ↔ ¬q.

Русский

Отрицание сохраняет эквивалентность: если p ↔ q, то ¬p ↔ ¬q.

LaTeX

$$$ (p \\leftrightarrow q) \\Rightarrow (\\\\neg p \\leftrightarrow \\\\neg q) $$$

Lean4

theorem rel_not : (Iff ⇒ Iff) Not Not := fun _ _ h => not_congr h

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

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

Разделы

Аффилиация

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