inlₗ — Mathlib

English

The left injection into the Lexicographic sum is defined by applying the lex-embedding to inl x, i.e., inlₗ(x) := toLex(inl x).

Русский

Левая инъекция в лексикографическую сумму задаётся как отображение inl x в лексикографическую сумму: inlₗ(x) = toLex(inl x).

LaTeX

$$$\mathrm{inl}_{\ell}(x) = \mathrm{toLex}(\mathrm{Sum.inl}(x)).$$$

Lean4

/-- Lexicographical `Sum.inl`. Only used for pattern matching. -/
@[match_pattern]
abbrev _root_.Sum.inlₗ (x : α) : α ⊕ₗ β :=
  toLex (Sum.inl x)

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