instLocallyFiniteOrderTop — Mathlib

English

In the dual order, the Ioc interval equals the map of the Ico interval from the original order.

Русский

В двойственном порядке интервал Ioc эквивалентен отображению интервала Ico из исходного порядка.

LaTeX

$$$ Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding $$$

Lean4

/-- Note we define `Ici (toDual a)` as `Iic a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Iic a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Ici (toDual (toDual a)) :) = (Ici a :) := rfl
```
-/
instance instLocallyFiniteOrderTop : LocallyFiniteOrderTop αᵒᵈ
    where
  finsetIci a := @Iic α _ _ (ofDual a)
  finsetIoi a := @Iio α _ _ (ofDual a)
  finset_mem_Ici _ _ := mem_Iic (α := α)
  finset_mem_Ioi _ _ := mem_Iio (α := α)

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