not_inl_le_inr

Mathlib.Data.Sum.Order

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem not_inl_le_inr [LE α] [LE β] {a : α} {b : β} : ¬inl b ≤ inr a :=
  not_liftRel_inl_inr

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

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

Разделы

Аффилиация

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