instLocallyFiniteOrderBot — Mathlib

English

In Lex, the closed down-set below a left-embedded a equals the image of the closed down-set below a under the left embedding composed with toLex.

Русский

В Lex замкнутое множество ниже левая встроенная точка эквивалентно изображению замкнутого множества ниже этой точки через встроение inl и toLex.

LaTeX

$$$ \operatorname{Iic}(\mathrm{inl}_\ell a) = (\operatorname{Iic} a).\mathrm{map}(\mathrm{Embedding.inl} .\mathrm{trans} toLex.toEmbedding) $$$

Lean4

instance instLocallyFiniteOrderBot : LocallyFiniteOrderBot (α ⊕ₗ β)
    where
  finsetIic :=
    Sum.elim (Iic · |>.map (.trans .inl toLex.toEmbedding))
        (fun x => Finset.univ.disjSum (Iic x) |>.map toLex.toEmbedding) ∘
      ofLex
  finsetIio :=
    Sum.elim (Iio · |>.map (.trans .inl toLex.toEmbedding))
        (fun x => Finset.univ.disjSum (Iio x) |>.map toLex.toEmbedding) ∘
      ofLex
  finset_mem_Iic := by simp
  finset_mem_Iio := by simp

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