sumLexIicIoi_symm_apply_Ioi — Mathlib

English

Let α be a linear order and x ∈ α. The inverse of the lexicographic sum map sends every element a of the right piece Ioi(x) to the right-injected element.

Русский

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

LaTeX

$$$(\mathrm{sumLexIicIoi}(x))^{-1}(a) = \mathrm{inr}(a), \quad a \in Ioi(x).$$$

Lean4

@[simp]
theorem sumLexIicIoi_symm_apply_Ioi (a : Ioi x) : (sumLexIicIoi x).symm a = Sum.inr a :=
  sumLexIicIoi_symm_apply_of_lt a.2

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