not_beq_of_ne

Mathlib.Logic.Basic

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

English

If a ≠ b, then the boolean equality test a == b evaluates to false.

Русский

Если a ≠ b, то булевое равенство a == b даёт значение ложь.

LaTeX

$$$ a \neq b \Rightarrow (a == b) = \text{Bool.false} $$$

Lean4

theorem not_beq_of_ne {α : Type*} [BEq α] [LawfulBEq α] {a b : α} (ne : a ≠ b) : ¬(a == b) := fun h => ne (eq_of_beq h)

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

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

Разделы

Аффилиация

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