English
The HasUpperLowerClosure property is transferred to order duals: the order dual α^op inherits HasUpperLowerClosure.
Русский
Свойство HasUpperLowerClosure переносится на двойственный порядок: порядок-двойственный α^op наследует HasUpperLowerClosure.
LaTeX
$$$HasUpperLowerClosure\\;\\alpha \\;\\Rightarrow\\; HasUpperLowerClosure(\\text{OrderDual } \\alpha)$$$
Lean4
@[to_additive]
instance (priority := 100) to_hasUpperLowerClosure [CommGroup α] [PartialOrder α] [IsOrderedMonoid α]
[ContinuousConstSMul α α] : HasUpperLowerClosure α
where
isUpperSet_closure s h x y hxy
hx :=
closure_mono (h.smul_subset <| one_le_div'.2 hxy) <|
by
rw [closure_smul]
exact ⟨x, hx, div_mul_cancel _ _⟩
isLowerSet_closure s h x y hxy
hx :=
closure_mono (h.smul_subset <| div_le_one'.2 hxy) <|
by
rw [closure_smul]
exact ⟨x, hx, div_mul_cancel _ _⟩
isOpen_upperClosure s
hs := by
rw [← mul_one s, ← mul_upperClosure]
exact hs.mul_right
isOpen_lowerClosure s
hs := by
rw [← mul_one s, ← mul_lowerClosure]
exact hs.mul_right
