sumLexIicIoi_symm_apply_Iic — Mathlib

English

Let α be a linear order and x ∈ α. The inverse of the lexicographic sum map that splits at x sends every element a of the left piece Iic(x) to the left-injected element.

Русский

Пусть α — линейно упорядоченное множество и x ∈ α. Обратное отображение лексикографического разбиения на пары слева отправляет каждый элемент a из Iic(x) в левую инъекцию.

LaTeX

$$$(\mathrm{inverses\,map\,of\,the\,lexicographic\,sum})^{-1}(a) = \mathrm{inl}(a), \quad a \in Iic(x).$$$

Lean4

@[simp]
theorem sumLexIicIoi_symm_apply_Iic (a : Iic x) : (sumLexIicIoi x).symm a = Sum.inl a :=
  sumLexIicIoi_symm_apply_of_le a.2

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