English
The instance provides HasUpperLowerClosure for the order dual αᵒᵈ.
Русский
Для двойственного порядка αᵒᵈ выполняется HasUpperLowerClosure.
LaTeX
$$$HasUpperLowerClosure\\;\\alpha \\Rightarrow HasUpperLowerClosure(\\alpha^{\\mathrm{op}})$$$
Lean4
instance : HasUpperLowerClosure αᵒᵈ
where
isUpperSet_closure := @IsLowerSet.closure α _ _ _
isLowerSet_closure := @IsUpperSet.closure α _ _ _
isOpen_upperClosure := @IsOpen.lowerClosure α _ _ _
isOpen_lowerClosure :=
@IsOpen.upperClosure α _ _
_
/-
Note: `s.OrdConnected` does not imply `(closure s).OrdConnected`, as we can see by taking
`s := Ioo 0 1 × Ioo 1 2 ∪ Ioo 2 3 × Ioo 0 1` because then
`closure s = Icc 0 1 × Icc 1 2 ∪ Icc 2 3 × Icc 0 1` is not order-connected as
`(1, 1) ∈ closure s`, `(2, 1) ∈ closure s` but `Icc (1, 1) (2, 1) ⊈ closure s`.
`s` looks like
```
xxooooo
xxooooo
oooooxx
oooooxx
```
-/
