/
UpperLower.lean
114 lines (93 loc) · 4.62 KB
/
UpperLower.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Algebra.Order.UpperLower
import Mathlib.Topology.Algebra.Group.Basic
#align_import topology.algebra.order.upper_lower from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"
/-!
# Topological facts about upper/lower/order-connected sets
The topological closure and interior of an upper/lower/order-connected set is an
upper/lower/order-connected set (with the notable exception of the closure of an order-connected
set).
## Implementation notes
The same lemmas are true in the additive/multiplicative worlds. To avoid code duplication, we
provide `HasUpperLowerClosure`, an ad hoc axiomatisation of the properties we need.
-/
open Function Set
open Pointwise
/-- Ad hoc class stating that the closure of an upper set is an upper set. This is used to state
lemmas that do not mention algebraic operations for both the additive and multiplicative versions
simultaneously. If you find a satisfying replacement for this typeclass, please remove it! -/
class HasUpperLowerClosure (α : Type*) [TopologicalSpace α] [Preorder α] : Prop where
isUpperSet_closure : ∀ s : Set α, IsUpperSet s → IsUpperSet (closure s)
isLowerSet_closure : ∀ s : Set α, IsLowerSet s → IsLowerSet (closure s)
isOpen_upperClosure : ∀ s : Set α, IsOpen s → IsOpen (upperClosure s : Set α)
isOpen_lowerClosure : ∀ s : Set α, IsOpen s → IsOpen (lowerClosure s : Set α)
#align has_upper_lower_closure HasUpperLowerClosure
variable {α : Type*} [TopologicalSpace α]
-- See note [lower instance priority]
@[to_additive]
instance (priority := 100) OrderedCommGroup.to_hasUpperLowerClosure [OrderedCommGroup α]
[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
#align ordered_comm_group.to_has_upper_lower_closure OrderedCommGroup.to_hasUpperLowerClosure
#align ordered_add_comm_group.to_has_upper_lower_closure OrderedAddCommGroup.to_hasUpperLowerClosure
variable [Preorder α] [HasUpperLowerClosure α] {s : Set α}
protected theorem IsUpperSet.closure : IsUpperSet s → IsUpperSet (closure s) :=
HasUpperLowerClosure.isUpperSet_closure _
#align is_upper_set.closure IsUpperSet.closure
protected theorem IsLowerSet.closure : IsLowerSet s → IsLowerSet (closure s) :=
HasUpperLowerClosure.isLowerSet_closure _
#align is_lower_set.closure IsLowerSet.closure
protected theorem IsOpen.upperClosure : IsOpen s → IsOpen (upperClosure s : Set α) :=
HasUpperLowerClosure.isOpen_upperClosure _
#align is_open.upper_closure IsOpen.upperClosure
protected theorem IsOpen.lowerClosure : IsOpen s → IsOpen (lowerClosure s : Set α) :=
HasUpperLowerClosure.isOpen_lowerClosure _
#align is_open.lower_closure IsOpen.lowerClosure
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
```
-/
protected theorem IsUpperSet.interior (h : IsUpperSet s) : IsUpperSet (interior s) := by
rw [← isLowerSet_compl, ← closure_compl]
exact h.compl.closure
#align is_upper_set.interior IsUpperSet.interior
protected theorem IsLowerSet.interior (h : IsLowerSet s) : IsLowerSet (interior s) :=
h.toDual.interior
#align is_lower_set.interior IsLowerSet.interior
protected theorem Set.OrdConnected.interior (h : s.OrdConnected) : (interior s).OrdConnected := by
rw [← h.upperClosure_inter_lowerClosure, interior_inter]
exact
(upperClosure s).upper.interior.ordConnected.inter (lowerClosure s).lower.interior.ordConnected
#align set.ord_connected.interior Set.OrdConnected.interior