locallyFiniteOrder — Mathlib

English

In the Lexicographic sum, the closed interval between two left-embedded elements equals the image of the corresponding interval in α under the composed embedding into the Lex sum.

Русский

В лексикографической сумме закрытый интервал между двумя элементами слева встроенными равен образу соответствующего интервала в α под композиционным встроением в сумму Lex.

LaTeX

$$$ \operatorname{Icc}(\mathrm{inl}_\ell a_1)(\mathrm{inl}_\ell a_2) = \operatorname{map}(\mathrm{Embedding.inl} \circ toLex.toEmbedding)(\operatorname{Icc} a_1 a_2) $$$

Lean4

instance locallyFiniteOrder : LocallyFiniteOrder (α ⊕ₗ β)
    where
  finsetIcc a b := (sumLexLift Icc Icc (fun a _ => Ici a) (fun _ => Iic) (ofLex a) (ofLex b)).map toLex.toEmbedding
  finsetIco a b := (sumLexLift Ico Ico (fun a _ => Ici a) (fun _ => Iio) (ofLex a) (ofLex b)).map toLex.toEmbedding
  finsetIoc a b := (sumLexLift Ioc Ioc (fun a _ => Ioi a) (fun _ => Iic) (ofLex a) (ofLex b)).map toLex.toEmbedding
  finsetIoo a b := (sumLexLift Ioo Ioo (fun a _ => Ioi a) (fun _ => Iio) (ofLex a) (ofLex b)).map toLex.toEmbedding
  finset_mem_Icc := by simp
  finset_mem_Ico := by simp
  finset_mem_Ioc := by simp
  finset_mem_Ioo := by simp

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