instLocallyFiniteOrder — Mathlib

English

The closed down-interval to b, Iic b, is finite in a locally finite order with bottom.

Русский

Замкнутый интервал снизу до b, Iic b, конечен в локально конечном порядке с нижней границей.

LaTeX

$$$\forall b \in \alpha, \lvert \{ x \in \alpha \mid x \le b \} \rvert < \infty$$$

Lean4

/-- Note we define `Icc (toDual a) (toDual b)` as `Icc α _ _ b a` (which has type `Finset α` not
`Finset αᵒᵈ`!) instead of `(Icc b a).map toDual.toEmbedding` as this means the
following is defeq:
```
lemma this : (Icc (toDual (toDual a)) (toDual (toDual b)) :) = (Icc a b :) := rfl
```
-/
instance instLocallyFiniteOrder : LocallyFiniteOrder αᵒᵈ
    where
  finsetIcc a b := @Icc α _ _ (ofDual b) (ofDual a)
  finsetIco a b := @Ioc α _ _ (ofDual b) (ofDual a)
  finsetIoc a b := @Ico α _ _ (ofDual b) (ofDual a)
  finsetIoo a b := @Ioo α _ _ (ofDual b) (ofDual a)
  finset_mem_Icc _ _ _ := (mem_Icc (α := α)).trans and_comm
  finset_mem_Ico _ _ _ := (mem_Ioc (α := α)).trans and_comm
  finset_mem_Ioc _ _ _ := (mem_Ico (α := α)).trans and_comm
  finset_mem_Ioo _ _ _ := (mem_Ioo (α := α)).trans and_comm

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