not_inl_lt_inr

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#Sum.not_inl_lt_inr

English

There is no strict inequality from the left to the right injection: ¬(inl b < inr a) for any a,b.

Русский

Нет строгого неравенства между левой и правой инъекциями: ¬(inl b < inr a) для любых a,b.

LaTeX

$$$\neg(\mathrm{inl}\,b < \mathrm{inr}\,a)$$$

Lean4

@[simp]
theorem not_inl_lt_inr [LT α] [LT β] {a : α} {b : β} : ¬inl b < inr a :=
  not_liftRel_inl_inr

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

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

Разделы

Аффилиация

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