ne

Mathlib.Logic.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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