Skip to content

Commit 4a6daef

Browse files
j-loreauxj-loreaux
committed
move WithBot and WithTop 
1 parent eda5b56 commit 4a6daef

File tree

2 files changed

+86
-88
lines changed

2 files changed

+86
-88
lines changed

‎Mathlib/Order/ConditionallyCompleteLattice/Basic.lean‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,92 @@ open Function OrderDual Set
3737

3838
variable {α β γ : Type*} {ι : Sort*}
3939

40+
section
41+
42+
/-!
43+
Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`
44+
-/
45+
46+
variable [Preorder α]
47+
48+
open Classical in
49+
noncomputable instance WithTop.instSupSet [SupSet α] :
50+
SupSet (WithTop α) :=
51+
⟨fun S =>
52+
if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then
53+
↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩
54+
55+
open Classical in
56+
noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
57+
⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
58+
59+
noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
60+
⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩
61+
62+
noncomputable instance WithBot.instInfSet [InfSet α] :
63+
InfSet (WithBot α) :=
64+
⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩
65+
66+
theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)
67+
(hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
68+
(if_neg hs).trans <| if_pos hs'
69+
70+
theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
71+
sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
72+
if_neg <| by simp [hs, h's]
73+
74+
theorem WithBot.sInf_eq [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s)
75+
(hs' : BddBelow ((↑) ⁻¹' s : Set α)) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
76+
(if_neg hs).trans <| if_pos hs'
77+
78+
theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
79+
sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
80+
WithTop.sInf_eq (α := αᵒᵈ) hs h's
81+
82+
@[simp]
83+
theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
84+
if_pos <| by simp
85+
86+
theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
87+
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
88+
classical
89+
obtain ⟨x, hx⟩ := hs
90+
change _ = ite _ _ _
91+
split_ifs with h
92+
· rcases h with h1 | h2
93+
· cases h1 (mem_image_of_mem _ hx)
94+
· exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
95+
· rw [preimage_image_eq]
96+
exact Option.some_injective _
97+
98+
theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
99+
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
100+
classical
101+
change _ = ite _ _ _
102+
rw [if_neg, preimage_image_eq, if_pos hs]
103+
· exact Option.some_injective _
104+
· rintro ⟨x, _, ⟨⟩⟩
105+
106+
@[simp]
107+
theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
108+
WithTop.sInf_empty (α := αᵒᵈ)
109+
110+
theorem WithBot.sInf_empty (α : Type*) [CompleteLattice α] : (sInf ∅ : WithBot α) = ⊤ := by
111+
rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
112+
WithBot.coe_top]
113+
114+
@[norm_cast]
115+
theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
116+
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
117+
WithTop.coe_sInf' (α := αᵒᵈ) hs h's
118+
119+
@[norm_cast]
120+
theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
121+
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
122+
WithTop.coe_sSup' (α := αᵒᵈ) hs
123+
124+
end
125+
40126
instance ConditionallyCompleteLinearOrder.toLinearOrder [h : ConditionallyCompleteLinearOrder α] :
41127
LinearOrder α where
42128
min_def a b := by

‎Mathlib/Order/ConditionallyCompletePartialOrder/Basic.lean‎

Lines changed: 0 additions & 88 deletions
Original file line numberDiff line numberDiff line change
@@ -30,94 +30,6 @@ open Function OrderDual Set
3030

3131
variable {α β γ : Type*} {ι : Sort*}
3232

33-
section
34-
35-
/-!
36-
Extension of `sSup` and `sInf` from a preorder `α` to `WithTop α` and `WithBot α`
37-
-/
38-
39-
variable [Preorder α]
40-
41-
open Classical in
42-
noncomputable instance WithTop.instSupSet [SupSet α] :
43-
SupSet (WithTop α) :=
44-
⟨fun S =>
45-
if ⊤ ∈ S then ⊤ else if BddAbove ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α) then
46-
↑(sSup ((fun (a : α) ↦ (a : WithTop α)) ⁻¹' S : Set α)) else ⊤⟩
47-
48-
open Classical in
49-
noncomputable instance WithTop.instInfSet [InfSet α] : InfSet (WithTop α) :=
50-
⟨fun S => if S ⊆ {⊤} ∨ ¬BddBelow S then ⊤ else ↑(sInf ((fun (a : α) ↦ ↑a) ⁻¹' S : Set α))⟩
51-
52-
noncomputable instance WithBot.instSupSet [SupSet α] : SupSet (WithBot α) :=
53-
⟨(WithTop.instInfSet (α := αᵒᵈ)).sInf⟩
54-
55-
noncomputable instance WithBot.instInfSet [InfSet α] :
56-
InfSet (WithBot α) :=
57-
⟨(WithTop.instSupSet (α := αᵒᵈ)).sSup⟩
58-
59-
theorem WithTop.sSup_eq [SupSet α] {s : Set (WithTop α)} (hs : ⊤ ∉ s)
60-
(hs' : BddAbove ((↑) ⁻¹' s : Set α)) : sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
61-
(if_neg hs).trans <| if_pos hs'
62-
63-
theorem WithTop.sInf_eq [InfSet α] {s : Set (WithTop α)} (hs : ¬s ⊆ {⊤}) (h's : BddBelow s) :
64-
sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
65-
if_neg <| by simp [hs, h's]
66-
67-
theorem WithBot.sInf_eq [InfSet α] {s : Set (WithBot α)} (hs : ⊥ ∉ s)
68-
(hs' : BddBelow ((↑) ⁻¹' s : Set α)) : sInf s = ↑(sInf ((↑) ⁻¹' s) : α) :=
69-
(if_neg hs).trans <| if_pos hs'
70-
71-
theorem WithBot.sSup_eq [SupSet α] {s : Set (WithBot α)} (hs : ¬s ⊆ {⊥}) (h's : BddAbove s) :
72-
sSup s = ↑(sSup ((↑) ⁻¹' s) : α) :=
73-
WithTop.sInf_eq (α := αᵒᵈ) hs h's
74-
75-
@[simp]
76-
theorem WithTop.sInf_empty [InfSet α] : sInf (∅ : Set (WithTop α)) = ⊤ :=
77-
if_pos <| by simp
78-
79-
theorem WithTop.coe_sInf' [InfSet α] {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
80-
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
81-
classical
82-
obtain ⟨x, hx⟩ := hs
83-
change _ = ite _ _ _
84-
split_ifs with h
85-
· rcases h with h1 | h2
86-
· cases h1 (mem_image_of_mem _ hx)
87-
· exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
88-
· rw [preimage_image_eq]
89-
exact Option.some_injective _
90-
91-
theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
92-
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α) := by
93-
classical
94-
change _ = ite _ _ _
95-
rw [if_neg, preimage_image_eq, if_pos hs]
96-
· exact Option.some_injective _
97-
· rintro ⟨x, _, ⟨⟩⟩
98-
99-
@[simp]
100-
theorem WithBot.sSup_empty [SupSet α] : sSup (∅ : Set (WithBot α)) = ⊥ :=
101-
WithTop.sInf_empty (α := αᵒᵈ)
102-
103-
theorem WithBot.sInf_empty (α : Type*) [CompleteLattice α] : (sInf ∅ : WithBot α) = ⊤ := by
104-
rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
105-
WithBot.coe_top]
106-
107-
@[norm_cast]
108-
theorem WithBot.coe_sSup' [SupSet α] {s : Set α} (hs : s.Nonempty) (h's : BddAbove s) :
109-
↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
110-
WithTop.coe_sInf' (α := αᵒᵈ) hs h's
111-
112-
@[norm_cast]
113-
theorem WithBot.coe_sInf' [InfSet α] {s : Set α} (hs : BddBelow s) :
114-
↑(sInf s) = (sInf ((fun (a : α) ↦ ↑a) '' s) : WithBot α) :=
115-
WithTop.coe_sSup' (α := αᵒᵈ) hs
116-
117-
end
118-
119-
variable {α : Type*}
120-
12133
namespace OrderDual
12234

12335
instance [ConditionallyCompletePartialOrderSup α] :

0 commit comments

Comments
 (0)
⚡