English
The right injection into the Lexicographic sum is defined by applying the lex-embedding to inr x, i.e., inrₗ(x) := toLex(inr x).
Русский
Правая инъекция в лексикографическую сумму задаётся как отображение inr x в лексикографическую сумму: inrₗ(x) = toLex(inr x).
LaTeX
$$$\mathrm{inr}_{\ell}(x) = \mathrm{toLex}(\mathrm{Sum.inr}(x)).$$$
Lean4
/-- Lexicographical `Sum.inr`. Only used for pattern matching. -/
@[match_pattern]
abbrev _root_.Sum.inrₗ (x : β) : α ⊕ₗ β :=
toLex (Sum.inr x)