ne_left

Mathlib.Logic.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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