not_inr_lt_inl — Mathlib

English

It is not the case that toLex(inr b) < toLex(inl a) for any a,b; i.e., inr cannot be strictly less than inl.

Русский

Не выполняется строгая неравенство toLex(inr b) < toLex(inl a) для любых a,b; то есть inr не меньше чем inl.

LaTeX

$$¬(toLex(\mathrm{Sum.inr}(b)) < toLex(\mathrm{Sum.inl}(a))).$$

Lean4

theorem not_inr_lt_inl [LT α] [LT β] {a : α} {b : β} : ¬toLex (inr b) < toLex (inl a) :=
  lex_inr_inl

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