Skip to content

Commit 7564dfc

Browse files
vihdzpvihdzp
committed
merge
1 parent 545b843 commit 7564dfc

1 file changed

Lines changed: 350 additions & 0 deletions

File tree

‎Mathlib/Order/DirSupClosed.lean‎

Lines changed: 350 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,350 @@
1+
/-
2+
Copyright (c) 2023 Christopher Hoskin. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Christopher Hoskin, Violeta Hernández Palacios
5+
-/
6+
module
7+
8+
public import Mathlib.Order.Antisymmetrization
9+
public import Mathlib.Order.CompleteLattice.Defs
10+
public import Mathlib.Order.UpperLower.Basic
11+
12+
import Mathlib.Data.Set.Lattice
13+
14+
/-!
15+
# Sets closed under directed suprema
16+
17+
We say that a set `s` is closed under directed suprema whenever it contains all least upper bounds
18+
for nonempty, directed subsets. Conversely, a set `s` is inaccessible by directed suprema whenever
19+
its complement is closed under directed suprema. Equivalently, if the least upper bound of a
20+
nonempty directed set `t` is contained in `s`, then `t` and `s` must have nonempty intersection.
21+
22+
## Main definitions
23+
24+
- `DirSupClosed`: sets closed under directed suprema.
25+
- `DirSupInacc`: sets inaccessible by directed suprema.
26+
-/
27+
28+
@[expose] public section
29+
30+
variable {α : Type*} {s t : Set α} {D D₁ D₂ : Set (Set α)}
31+
32+
open Set
33+
34+
section Preorder
35+
variable [Preorder α]
36+
37+
/-- A predicate for a set which is closed under directed suprema of nonempty sets.
38+
This is the complement of a `DirSupInaccOn` set. -/
39+
def DirSupClosedOn (D : Set (Set α)) (s : Set α) : Prop :=
40+
∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s
41+
42+
/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets in `D`.
43+
This is the complement of a `DirSupClosedOn` set. -/
44+
def DirSupInaccOn (D : Set (Set α)) (s : Set α) : Prop :=
45+
∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
46+
47+
/-- A predicate for a set which is closed under directed suprema of nonempty sets.
48+
This is the complement of a `DirSupInacc` set. -/
49+
def DirSupClosed (s : Set α) : Prop :=
50+
∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s
51+
52+
/-- A predicate for a set which is inaccessible by directed suprema of nonempty sets.
53+
This is the complement of a `DirSupClosed` set. -/
54+
def DirSupInacc (s : Set α) : Prop :=
55+
∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty
56+
57+
@[simp] lemma dirSupClosedOn_univ : DirSupClosedOn univ s ↔ DirSupClosed s := by
58+
simp [DirSupClosedOn, DirSupClosed]
59+
60+
@[simp] lemma dirSupInaccOn_univ : DirSupInaccOn univ s ↔ DirSupInacc s := by
61+
simp [DirSupInaccOn, DirSupInacc]
62+
63+
@[simp] lemma DirSupClosed.dirSupClosedOn : DirSupClosed s → DirSupClosedOn D s := @fun h _ _ ↦ @h _
64+
@[simp] lemma DirSupInacc.dirSupInaccOn : DirSupInacc s → DirSupInaccOn D s := @fun h _ _ ↦ @h _
65+
66+
@[simp] theorem DirSupClosed.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosed s :=
67+
fun _ _ ⟨a, _⟩ ↦ isEmptyElim a
68+
69+
@[simp] theorem DirSupInacc.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInacc s :=
70+
fun _ ⟨a, _⟩ ↦ isEmptyElim a
71+
72+
theorem DirSupClosedOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupClosedOn D s := by simp
73+
theorem DirSupInaccOn.of_isEmpty [IsEmpty α] {s : Set α} : DirSupInaccOn D s := by simp
74+
75+
@[gcongr]
76+
lemma DirSupClosedOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupClosedOn D₂ s) : DirSupClosedOn D₁ s :=
77+
fun _ a ↦ hf (hD a)
78+
79+
@[gcongr]
80+
lemma DirSupInaccOn.mono (hD : D₁ ⊆ D₂) (hf : DirSupInaccOn D₂ s) : DirSupInaccOn D₁ s :=
81+
fun _ a ↦ hf (hD a)
82+
83+
@[simp]
84+
lemma dirSupClosedOn_compl : DirSupClosedOn D sᶜ ↔ DirSupInaccOn D s := by
85+
simp_rw [DirSupClosedOn, DirSupInaccOn, ← not_disjoint_iff_nonempty_inter]
86+
grind
87+
88+
@[simp]
89+
lemma dirSupClosed_compl : DirSupClosed sᶜ ↔ DirSupInacc s := by
90+
rw [← dirSupClosedOn_univ, dirSupClosedOn_compl, dirSupInaccOn_univ]
91+
92+
@[simp]
93+
lemma dirSupInaccOn_compl : DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s := by
94+
rw [← dirSupClosedOn_compl, compl_compl]
95+
96+
@[simp]
97+
lemma dirSupInacc_compl : DirSupInacc sᶜ ↔ DirSupClosed s := by
98+
rw [← dirSupClosed_compl, compl_compl]
99+
100+
alias ⟨DirSupInaccOn.of_compl, DirSupInaccOn.compl⟩ := dirSupClosedOn_compl
101+
alias ⟨DirSupClosedOn.of_compl, DirSupClosedOn.compl⟩ := dirSupInaccOn_compl
102+
alias ⟨DirSupInacc.of_compl, DirSupInacc.compl⟩ := dirSupClosed_compl
103+
alias ⟨DirSupClosed.of_compl, DirSupClosed.compl⟩ := dirSupInacc_compl
104+
105+
@[simp] theorem DirSupClosed.empty : DirSupClosed (∅ : Set α) := by simp [DirSupClosed]
106+
@[simp] theorem DirSupInacc.empty : DirSupInacc (∅ : Set α) := by simp [DirSupInacc]
107+
theorem DirSupClosedOn.empty : DirSupClosedOn D ∅ := by simp
108+
theorem DirSupInaccOn.empty : DirSupInaccOn D ∅ := by simp
109+
110+
@[simp] theorem DirSupClosed.univ : DirSupClosed (univ : Set α) := by simp [DirSupClosed]
111+
@[simp] theorem DirSupInacc.univ : DirSupInacc (univ : Set α) := by simp [← compl_empty]
112+
theorem DirSupClosedOn.univ : DirSupClosedOn D univ := by simp
113+
theorem DirSupInaccOn.univ : DirSupInaccOn D univ := by simp
114+
115+
theorem DirSupClosedOn.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosedOn D x) :
116+
DirSupClosedOn D (⋂₀ s) :=
117+
fun _d hD hds hd hd' _a ha t ht ↦ hs t ht hD (hds.trans fun _x hx ↦ hx _ ht) hd hd' ha
118+
119+
theorem DirSupClosed.sInter {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupClosed x) :
120+
DirSupClosed (⋂₀ s) := by
121+
simpa using DirSupClosedOn.sInter fun x hx ↦ (hs x hx).dirSupClosedOn (D := .univ)
122+
123+
theorem DirSupInaccOn.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInaccOn D x) :
124+
DirSupInaccOn D (⋃₀ s) := by
125+
rw [← dirSupClosedOn_compl, Set.compl_sUnion]
126+
apply DirSupClosedOn.sInter
127+
rintro x ⟨x, hx, rfl⟩
128+
exact (hs x hx).compl
129+
130+
theorem DirSupInacc.sUnion {s : Set (Set α)} (hs : ∀ x ∈ s, DirSupInacc x) :
131+
DirSupInacc (⋃₀ s) := by
132+
simpa using DirSupInaccOn.sUnion fun x hx ↦ (hs x hx).dirSupInaccOn (D := .univ)
133+
134+
theorem DirSupClosedOn.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosedOn D (f i)) :
135+
DirSupClosedOn D (⋂ i, f i) := by
136+
rw [← sInter_range f]
137+
exact DirSupClosedOn.sInter (by simpa)
138+
139+
theorem DirSupClosed.iInter {ι} {f : ι → Set α} (hs : ∀ i, DirSupClosed (f i)) :
140+
DirSupClosed (⋂ i, f i) := by
141+
rw [← sInter_range f]
142+
exact DirSupClosed.sInter (by simpa)
143+
144+
theorem DirSupInaccOn.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInaccOn D (f i)) :
145+
DirSupInaccOn D (⋃ i, f i) := by
146+
rw [← sUnion_range f]
147+
exact DirSupInaccOn.sUnion (by simpa)
148+
149+
theorem DirSupInacc.iUnion {ι} {f : ι → Set α} (hs : ∀ i, DirSupInacc (f i)) :
150+
DirSupInacc (⋃ i, f i) := by
151+
rw [← sUnion_range f]
152+
exact DirSupInacc.sUnion (by simpa)
153+
154+
lemma DirSupClosedOn.inter (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) :
155+
DirSupClosedOn D (s ∩ t) := by
156+
rw [← sInter_pair]
157+
refine .sInter ?_
158+
simpa [hs]
159+
160+
lemma DirSupClosed.inter (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∩ t) := by
161+
simpa using hs.dirSupClosedOn.inter ht.dirSupClosedOn (D := .univ)
162+
163+
lemma DirSupInaccOn.union (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) :
164+
DirSupInaccOn D (s ∪ t) := by
165+
rw [← dirSupClosedOn_compl, compl_union]; exact hs.compl.inter ht.compl
166+
167+
lemma DirSupInacc.union (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∪ t) := by
168+
simpa using hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ)
169+
170+
theorem DirSupClosedOn.union (hDL : IsLowerSet D)
171+
(hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : DirSupClosedOn D (s ∪ t) := by
172+
intro d hD hdu hd₀ hd₁ a ha
173+
have hdst : d ∩ s ∪ d ∩ t = d := by grind
174+
rw [← hdst] at hd₀ hd₁
175+
wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty
176+
· rw [union_comm] at hdu hd₀ hd₁ hdst ⊢
177+
exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
178+
(directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h
179+
obtain ⟨hds, hn⟩ := h
180+
by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s))
181+
· exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds
182+
⟨fun b hb ↦ ha.1 hb.1, had⟩
183+
· simp only [lowerBounds, mem_setOf_eq, not_forall] at had
184+
obtain ⟨b, hb, hb'⟩ := had
185+
have key : {x ∈ d | ¬ x ≤ b} ⊆ d ∩ t := fun a ⟨had, hab⟩ ↦
186+
⟨had, (hdu had).resolve_left fun has ↦ hab <| hb ⟨had, has⟩⟩
187+
obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by
188+
contrapose! hb'
189+
apply ha.2
190+
aesop
191+
refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right)
192+
⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_
193+
· obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy))
194+
exact ⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩
195+
· refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩
196+
by_cases hyb : y ≤ b
197+
· obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw))
198+
exact hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩)
199+
exact hx ⟨hy, hyb⟩
200+
201+
theorem DirSupInaccOn.inter (hDL : IsLowerSet D)
202+
(hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∩ t) := by
203+
rw [← dirSupClosedOn_compl, compl_inter]; exact hs.compl.union hDL ht.compl
204+
205+
theorem DirSupClosed.union (hs : DirSupClosed s) (ht : DirSupClosed t) : DirSupClosed (s ∪ t) := by
206+
simpa using hs.dirSupClosedOn.union isLowerSet_univ ht.dirSupClosedOn
207+
208+
theorem DirSupInacc.inter (hs : DirSupInacc s) (ht : DirSupInacc t) : DirSupInacc (s ∩ t) := by
209+
simpa using hs.dirSupInaccOn.inter isLowerSet_univ ht.dirSupInaccOn
210+
211+
theorem DirSupInaccOn.of_inter_subset
212+
(h : ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d →
213+
∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInaccOn D s := by
214+
intro d hd₀ hd₁ hd₂ a hda hd₃
215+
obtain ⟨b, hbd, hb⟩ := h hd₀ hd₁ hd₂ hda hd₃
216+
exact ⟨b, hbd, hb ⟨le_rfl, hbd⟩⟩
217+
218+
theorem DirSupInacc.of_inter_subset
219+
(h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d →
220+
∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s) : DirSupInacc s :=
221+
dirSupInaccOn_univ.1 (.of_inter_subset (by simpa))
222+
223+
/-- The condition `(d ∩ s).Nonempty` in `DirSupInaccOn` can be replaced with the stronger
224+
`∃ b ∈ d, Ici b ∩ d ⊆ s` (under mild assumptions on `D`). -/
225+
theorem dirSupInaccOn_iff_inter_subset (hDL : IsLowerSet D) :
226+
DirSupInaccOn D s ↔ ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d →
227+
∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s where
228+
mpr := .of_inter_subset
229+
mp h t hD ht₀ ht₁ a ha has := by
230+
by_contra! H
231+
have H : ∀ b : t, ∃ c, b.1 ≤ c ∧ c ∈ t ∧ c ∉ s := by simpa [not_subset, and_assoc] using H
232+
choose f hf using H
233+
have := ht₀.to_subtype
234+
have hft : range f ⊆ t := by grind
235+
apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty
236+
· aesop
237+
· intro a ha b hb
238+
obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb)
239+
have := hf ⟨c, hc⟩
240+
grind
241+
· exact ⟨upperBounds_mono_set hft ha.1,
242+
fun b hb ↦ ha.2 fun c hc ↦ (hf ⟨c, hc⟩).1.trans (hb <| by simp)⟩
243+
244+
/-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger
245+
`∃ b ∈ d, Ici b ∩ d ⊆ s`. -/
246+
theorem dirSupInacc_iff_inter_subset :
247+
DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d →
248+
∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s := by
249+
simpa using dirSupInaccOn_iff_inter_subset isLowerSet_univ
250+
251+
lemma IsUpperSet.dirSupClosed (hs : IsUpperSet s) : DirSupClosed s :=
252+
fun _d hds ⟨_b, hb⟩ _ _a ha ↦ hs (ha.1 hb) <| hds hb
253+
254+
lemma IsUpperSet.dirSupClosedOn (hs : IsUpperSet s) : DirSupClosedOn D s :=
255+
hs.dirSupClosed.dirSupClosedOn
256+
257+
lemma IsLowerSet.dirSupInacc (hs : IsLowerSet s) : DirSupInacc s :=
258+
.of_compl hs.compl.dirSupClosed
259+
260+
lemma IsLowerSet.dirSupInaccOn (hs : IsLowerSet s) : DirSupInaccOn D s :=
261+
.of_compl hs.compl.dirSupClosedOn
262+
263+
theorem DirSupClosed.mem_imp_of_antisymmRel (hs : DirSupClosed s) {a b : α}
264+
(h : AntisymmRel (· ≤ ·) a b) (ha : a ∈ s) : b ∈ s := by
265+
apply hs (singleton_subset_iff.2 ha) ⟨a, rfl⟩ (directedOn_singleton a)
266+
rw [← isLUB_congr_of_antisymmRel h]
267+
exact isLUB_singleton
268+
269+
theorem DirSupClosed.mem_iff_of_antisymmRel (hs : DirSupClosed s) {a b : α}
270+
(h : AntisymmRel (· ≤ ·) a b) : a ∈ s ↔ b ∈ s :=
271+
⟨hs.mem_imp_of_antisymmRel h, hs.mem_imp_of_antisymmRel h.symm⟩
272+
273+
theorem DirSupInacc.mem_iff_of_antisymmRel (hs : DirSupInacc s) {a b : α}
274+
(h : AntisymmRel (· ≤ ·) a b) : a ∈ s ↔ b ∈ s := by
275+
simpa [not_iff_not] using hs.compl.mem_iff_of_antisymmRel h
276+
277+
lemma dirSupClosed_Iic (a : α) : DirSupClosed (Iic a) :=
278+
fun _d h _ _ _a ha ↦ (isLUB_le_iff ha).2 h
279+
280+
lemma dirSupClosedOn_Iic (a : α) : DirSupClosedOn D (Iic a) :=
281+
(dirSupClosed_Iic a).dirSupClosedOn
282+
283+
lemma dirSupInacc_Iic (a : α) : DirSupInacc (Iic a) :=
284+
(isLowerSet_Iic a).dirSupInacc
285+
286+
lemma dirSupInaccOn_Iic (a : α) : DirSupInaccOn D (Iic a) :=
287+
(isLowerSet_Iic a).dirSupInaccOn
288+
289+
end Preorder
290+
291+
section PartialOrder
292+
variable [PartialOrder α]
293+
294+
theorem DirSupClosed.singleton (a : α) : DirSupClosed {a} := by
295+
intro d hda hdn _ b hb
296+
rw [hdn.subset_singleton_iff] at hda
297+
subst hda
298+
exact mem_singleton_of_eq (hb.unique isLUB_singleton)
299+
300+
@[deprecated (since := "2026-05-22")] alias dirSupClosed_singleton := DirSupClosed.singleton
301+
302+
theorem DirSupClosedOn.singleton (a : α) : DirSupClosedOn D {a} :=
303+
(DirSupClosed.singleton a).dirSupClosedOn
304+
305+
@[deprecated (since := "2026-05-22")] alias dirSupClosedOn_singleton := DirSupClosedOn.singleton
306+
307+
end PartialOrder
308+
309+
section LinearOrder
310+
variable [LinearOrder α]
311+
312+
theorem dirSupClosedOn_iff_of_linearOrder :
313+
DirSupClosedOn D s ↔ ∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by
314+
simp [DirSupClosedOn]
315+
316+
theorem dirSupClosed_iff_of_linearOrder :
317+
DirSupClosed s ↔ ∀ ⦃d⦄, d ⊆ s → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s := by
318+
simp [DirSupClosed]
319+
320+
theorem dirSupInaccOn_iff_of_linearOrder :
321+
DirSupInaccOn D s ↔
322+
∀ ⦃d⦄, d ∈ D → d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by
323+
simp [DirSupInaccOn]
324+
325+
theorem dirSupInacc_iff_of_linearOrder :
326+
DirSupInacc s ↔ ∀ ⦃d⦄, d.Nonempty → ∀ ⦃a⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty := by
327+
simp [DirSupInacc]
328+
329+
end LinearOrder
330+
331+
section CompleteLattice
332+
variable [CompleteLattice α]
333+
334+
lemma dirSupClosedOn_iff_forall_sSup : DirSupClosedOn D s ↔
335+
∀ ⦃d⦄, d ∈ D → d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s := by
336+
simp [DirSupClosedOn, isLUB_iff_sSup_eq]
337+
338+
lemma dirSupInaccOn_iff_forall_sSup : DirSupInaccOn D s ↔
339+
∀ ⦃d⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by
340+
simp [DirSupInaccOn, isLUB_iff_sSup_eq]
341+
342+
lemma dirSupClosed_iff_forall_sSup : DirSupClosed s ↔
343+
∀ ⦃d⦄, d ⊆ s → d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s := by
344+
simp [DirSupClosed, isLUB_iff_sSup_eq]
345+
346+
lemma dirSupInacc_iff_forall_sSup : DirSupInacc s ↔
347+
∀ ⦃d⦄, d.Nonempty → DirectedOn (· ≤ ·) d → sSup d ∈ s → (d ∩ s).Nonempty := by
348+
simp [DirSupInacc, isLUB_iff_sSup_eq]
349+
350+
end CompleteLattice

0 commit comments

Comments
 (0)