Ioi_inl — Mathlib

English

In the Lex sum, the Ioi (inl a) consists of all inl a′ with a < a′ together with all inr b, reflecting that any inr element is larger than any inl element in the Lex order.

Русский

В лексикографической сумме Ioi(inl a) содержит все inl a′ с a < a′ и все элементы inr b, поскольку любой inr бóльше любого inl в этом порядке.

LaTeX

$$$ Ioi\\bigl(\\mathrm{inl}_{\\ell}\\, a\\bigr) = \\bigl((\\Ioi\\, a) \\disjSum \\mathrm{univ}\\bigr).\\mathrm{map}\\;\\mathrm{toLex.toEmbedding}$$$

Lean4

theorem Ioi_inl : Ioi (inlₗ a : α ⊕ₗ β) = ((Ioi a).disjSum Finset.univ).map toLex.toEmbedding :=
  rfl

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