English
There exists a LocallyFiniteOrderBot structure on the dual order αᵒᵈ, obtained from α with LocallyFiniteOrderTop, by defining the lower and upper finsets via the dual embedding.
Русский
Существует структура LocallyFiniteOrderBot на двойственном порядке αᵒᵈ, получаемая из α с LocallyFiniteOrderTop, определяющая нижние и верхние конечные множества через двойственное вложение.
LaTeX
$$$ \operatorname{LocallyFiniteOrderBot}(\alpha^{\mathrm{op}}) $$$
Lean4
/-- Note we define `Iic (toDual a)` as `Ici a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Ici a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Iic (toDual (toDual a)) :) = (Iic a :) := rfl
```
-/
instance instLocallyFiniteOrderBot : LocallyFiniteOrderBot αᵒᵈ
where
finsetIic a := @Ici α _ _ (ofDual a)
finsetIio a := @Ioi α _ _ (ofDual a)
finset_mem_Iic _ _ := mem_Ici (α := α)
finset_mem_Iio _ _ := mem_Ioi (α := α)
