not_left

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#Iff.not_left

English

If a ≡ ¬b, then ¬a ≡ b.

Русский

Если a эквивалентно ¬b, тогда ¬a эквивалентно b.

LaTeX

$$$(a \leftrightarrow \lnot b) \Rightarrow (\lnot a \leftrightarrow b)$$$

Lean4

theorem not_left (h : a ↔ ¬b) : ¬a ↔ b :=
  h.not.trans not_not

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

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

Разделы

Аффилиация

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