ne_right

Mathlib.Logic.Basic

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

English

If a ≠ b ↔ c = d, then a = b ↔ c ≠ d.

Русский

Если a ≠ b ↔ c = d, то a = b ↔ c ≠ d.

LaTeX

$$(a \neq b \leftrightarrow c = d) \Rightarrow (a = b \leftrightarrow c \neq d)$$

Lean4

theorem ne_right {α β : Sort*} {a b : α} {c d : β} : (a ≠ b ↔ c = d) → (a = b ↔ c ≠ d) :=
  Iff.not_right

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

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

Разделы

Аффилиация

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