not_inr_le_inl

Mathlib.Data.Sum.Order

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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