inrₗ — Mathlib

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)

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