ne_and_eq_iff_right

Mathlib.Logic.Basic

URI: https://scilib.ai/kg/mathlib#ne_and_eq_iff_right

English

From a proof object Fact p, one can extract the underlying proposition p.

Русский

Из доказательства Fact p можно извлечь само утверждение p.

LaTeX

$$$ \\mathrm{Fact}\\ p \\;\\rightarrow\\; p. $$$

Lean4

theorem ne_and_eq_iff_right {a b c : α} (h : b ≠ c) : a ≠ b ∧ a = c ↔ a = c :=
  and_iff_right_of_imp (fun h2 => h2.symm ▸ h.symm)

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

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

Разделы

Аффилиация

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