ne_of_ne_of_eq'

Mathlib.Tactic.Positivity.Core

URI: https://scilib.ai/kg/mathlib#ne_of_ne_of_eq'

Lean4

theorem ne_of_ne_of_eq' {α : Sort*} {a c b : α} (hab : (a : α) ≠ c) (hbc : a = b) : b ≠ c :=
  hbc ▸ hab

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

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

Разделы

Аффилиация

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