inl_le_inr — Mathlib

English

For all a in α and b in β, we have toLex(inl a) ≤ toLex(inr b) (in particular, inl is always below inr).

Русский

Для всех a ∈ α и b ∈ β имеем toLex(inl a) ≤ toLex(inr b) (в частности inl всегда меньше чем inr).

LaTeX

$$$\forall a:\, a \in \alpha,\; \forall b:\, b \in \beta:\; toLex(\mathrm{Sum.inl}(a)) \le toLex(\mathrm{Sum.inr}(b)).$$$

Lean4

theorem inl_le_inr [LE α] [LE β] (a : α) (b : β) : toLex (inl a) ≤ toLex (inr b) :=
  Lex.sep _ _

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