English
Let α and β be preordered sets with finite and top/bottom structure as in the statement. In the lexicographic sum α ⊕β, the closed lower interval below inr b consists exactly of all left elements together with those right elements not exceeding b; equivalently, Iic(inr b) is obtained by taking all inl a (a ∈ α) and all inr b′ with b′ ≤ b, and embedding them into the lexicographic sum.
Русский
Пусть α и β образуют упорядоченные множества с заданными локальными свойствами. В лексикографическом суммировании α ⊕ β множество элементов, меньших или равных элементу inr b, состоит из всех элементов типа inl a (a ∈ α) и всех элементов типа inr b′, где b′ ≤ b; то есть Iic(inr b) получается как образ объединения α и Iic(b) под встраиванием в лексикографическое сложение.
LaTeX
$$$ I\\!i\\!c\\,\\bigl(\\mathrm{inr}_{\\ell}\\, b\\bigr) = \\bigl( \\mathrm{univ}.\\disjSum (Iic\\, b) \\bigr).\\mathrm{map}\\,\\mathrm{toLex.toEmbedding} $$$
Lean4
theorem Iic_inr : Iic (inrₗ b : α ⊕ₗ β) = (Finset.univ.disjSum (Iic b)).map toLex.toEmbedding :=
rfl
