not_inr_lt_inl

Mathlib.Data.Sum.Order

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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