cmpUsing_eq_eq

Mathlib.Data.Ordering.Lemmas

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

English

The equality cmpUsing lt a b = Ordering.eq is equivalent to not a < b and not b < a.

Русский

Равенство cmpUsing lt a b = Ordering.eq эквивалентно не a < b и не b < a.

LaTeX

$$$\\forall a,b,\\ (cmpUsing\\ lt\\ a\\ b = Ordering.eq) \\iff (\\neg (lt a b) \\land \\neg (lt b a))$$$

Lean4

@[simp]
theorem cmpUsing_eq_eq (a b : α) : cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a := by simp

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

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

Разделы

Аффилиация

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