/
partial.lean
212 lines (171 loc) · 8.25 KB
/
partial.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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
/-
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad
Extends `tendsto` to relations and partial functions.
-/
import order.filter.basic
universes u v w
namespace filter
variables {α : Type u} {β : Type v} {γ : Type w}
open_locale filter
/-
Relations.
-/
def rmap (r : rel α β) (f : filter α) : filter β :=
{ sets := r.core ⁻¹' f.sets,
univ_sets := by { simp [rel.core], apply univ_mem_sets },
sets_of_superset := assume s t hs st, mem_sets_of_superset hs $ rel.core_mono _ st,
inter_sets := by { simp [set.preimage, rel.core_inter], exact λ s t, inter_mem_sets } }
theorem rmap_sets (r : rel α β) (f : filter α) : (rmap r f).sets = r.core ⁻¹' f.sets := rfl
@[simp]
theorem mem_rmap (r : rel α β) (l : filter α) (s : set β) :
s ∈ l.rmap r ↔ r.core s ∈ l :=
iff.rfl
@[simp]
theorem rmap_rmap (r : rel α β) (s : rel β γ) (l : filter α) :
rmap s (rmap r l) = rmap (r.comp s) l :=
filter_eq $
by simp [rmap_sets, set.preimage, rel.core_comp]
@[simp]
lemma rmap_compose (r : rel α β) (s : rel β γ) : rmap s ∘ rmap r = rmap (r.comp s) :=
funext $ rmap_rmap _ _
def rtendsto (r : rel α β) (l₁ : filter α) (l₂ : filter β) := l₁.rmap r ≤ l₂
theorem rtendsto_def (r : rel α β) (l₁ : filter α) (l₂ : filter β) :
rtendsto r l₁ l₂ ↔ ∀ s ∈ l₂, r.core s ∈ l₁ :=
iff.rfl
def rcomap (r : rel α β) (f : filter β) : filter α :=
{ sets := rel.image (λ s t, r.core s ⊆ t) f.sets,
univ_sets := ⟨set.univ, univ_mem_sets, set.subset_univ _⟩,
sets_of_superset := assume a b ⟨a', ha', ma'a⟩ ab, ⟨a', ha', set.subset.trans ma'a ab⟩,
inter_sets := assume a b ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩,
⟨a' ∩ b', inter_mem_sets ha₁ hb₁,
set.subset.trans (by rw rel.core_inter)
(set.inter_subset_inter ha₂ hb₂)⟩ }
theorem rcomap_sets (r : rel α β) (f : filter β) :
(rcomap r f).sets = rel.image (λ s t, r.core s ⊆ t) f.sets := rfl
@[simp]
theorem rcomap_rcomap (r : rel α β) (s : rel β γ) (l : filter γ) :
rcomap r (rcomap s l) = rcomap (r.comp s) l :=
filter_eq $
begin
ext t, simp [rcomap_sets, rel.image, rel.core_comp], split,
{ rintros ⟨u, ⟨v, vsets, hv⟩, h⟩,
exact ⟨v, vsets, set.subset.trans (rel.core_mono _ hv) h⟩ },
rintros ⟨t, tsets, ht⟩,
exact ⟨rel.core s t, ⟨t, tsets, set.subset.refl _⟩, ht⟩
end
@[simp]
lemma rcomap_compose (r : rel α β) (s : rel β γ) : rcomap r ∘ rcomap s = rcomap (r.comp s) :=
funext $ rcomap_rcomap _ _
theorem rtendsto_iff_le_comap (r : rel α β) (l₁ : filter α) (l₂ : filter β) :
rtendsto r l₁ l₂ ↔ l₁ ≤ l₂.rcomap r :=
begin
rw rtendsto_def,
change (∀ (s : set β), s ∈ l₂.sets → rel.core r s ∈ l₁) ↔ l₁ ≤ rcomap r l₂,
simp [filter.le_def, rcomap, rel.mem_image], split,
intros h s t tl₂ h',
{ exact mem_sets_of_superset (h t tl₂) h' },
intros h t tl₂,
apply h _ t tl₂ (set.subset.refl _),
end
-- Interestingly, there does not seem to be a way to express this relation using a forward map.
-- Given a filter `f` on `α`, we want a filter `f'` on `β` such that `r.preimage s ∈ f` if
-- and only if `s ∈ f'`. But the intersection of two sets satsifying the lhs may be empty.
def rcomap' (r : rel α β) (f : filter β) : filter α :=
{ sets := rel.image (λ s t, r.preimage s ⊆ t) f.sets,
univ_sets := ⟨set.univ, univ_mem_sets, set.subset_univ _⟩,
sets_of_superset := assume a b ⟨a', ha', ma'a⟩ ab, ⟨a', ha', set.subset.trans ma'a ab⟩,
inter_sets := assume a b ⟨a', ha₁, ha₂⟩ ⟨b', hb₁, hb₂⟩,
⟨a' ∩ b', inter_mem_sets ha₁ hb₁,
set.subset.trans (@rel.preimage_inter _ _ r _ _)
(set.inter_subset_inter ha₂ hb₂)⟩ }
@[simp]
lemma mem_rcomap' (r : rel α β) (l : filter β) (s : set α) :
s ∈ l.rcomap' r ↔ ∃ t ∈ l, rel.preimage r t ⊆ s :=
iff.rfl
theorem rcomap'_sets (r : rel α β) (f : filter β) :
(rcomap' r f).sets = rel.image (λ s t, r.preimage s ⊆ t) f.sets := rfl
@[simp]
theorem rcomap'_rcomap' (r : rel α β) (s : rel β γ) (l : filter γ) :
rcomap' r (rcomap' s l) = rcomap' (r.comp s) l :=
filter_eq $
begin
ext t, simp [rcomap'_sets, rel.image, rel.preimage_comp], split,
{ rintros ⟨u, ⟨v, vsets, hv⟩, h⟩,
exact ⟨v, vsets, set.subset.trans (rel.preimage_mono _ hv) h⟩ },
rintros ⟨t, tsets, ht⟩,
exact ⟨rel.preimage s t, ⟨t, tsets, set.subset.refl _⟩, ht⟩
end
@[simp]
lemma rcomap'_compose (r : rel α β) (s : rel β γ) : rcomap' r ∘ rcomap' s = rcomap' (r.comp s) :=
funext $ rcomap'_rcomap' _ _
def rtendsto' (r : rel α β) (l₁ : filter α) (l₂ : filter β) := l₁ ≤ l₂.rcomap' r
theorem rtendsto'_def (r : rel α β) (l₁ : filter α) (l₂ : filter β) :
rtendsto' r l₁ l₂ ↔ ∀ s ∈ l₂, r.preimage s ∈ l₁ :=
begin
unfold rtendsto', unfold rcomap', simp [le_def, rel.mem_image], split,
{ intros h s hs, apply (h _ _ hs (set.subset.refl _)) },
intros h s t ht h', apply mem_sets_of_superset (h t ht) h'
end
theorem tendsto_iff_rtendsto (l₁ : filter α) (l₂ : filter β) (f : α → β) :
tendsto f l₁ l₂ ↔ rtendsto (function.graph f) l₁ l₂ :=
by { simp [tendsto_def, function.graph, rtendsto_def, rel.core, set.preimage] }
theorem tendsto_iff_rtendsto' (l₁ : filter α) (l₂ : filter β) (f : α → β) :
tendsto f l₁ l₂ ↔ rtendsto' (function.graph f) l₁ l₂ :=
by { simp [tendsto_def, function.graph, rtendsto'_def, rel.preimage_def, set.preimage] }
/-
Partial functions.
-/
def pmap (f : α →. β) (l : filter α) : filter β :=
filter.rmap f.graph' l
@[simp]
lemma mem_pmap (f : α →. β) (l : filter α) (s : set β) : s ∈ l.pmap f ↔ f.core s ∈ l :=
iff.rfl
def ptendsto (f : α →. β) (l₁ : filter α) (l₂ : filter β) := l₁.pmap f ≤ l₂
theorem ptendsto_def (f : α →. β) (l₁ : filter α) (l₂ : filter β) :
ptendsto f l₁ l₂ ↔ ∀ s ∈ l₂, f.core s ∈ l₁ :=
iff.rfl
theorem ptendsto_iff_rtendsto (l₁ : filter α) (l₂ : filter β) (f : α →. β) :
ptendsto f l₁ l₂ ↔ rtendsto f.graph' l₁ l₂ :=
iff.rfl
theorem pmap_res (l : filter α) (s : set α) (f : α → β) :
pmap (pfun.res f s) l = map f (l ⊓ 𝓟 s) :=
filter_eq $
begin
apply set.ext, intro t, simp [pfun.core_res], split,
{ intro h, constructor, split, { exact h },
constructor, split, { reflexivity },
simp [set.inter_distrib_right], apply set.inter_subset_left },
rintro ⟨t₁, h₁, t₂, h₂, h₃⟩, apply mem_sets_of_superset h₁, rw ← set.inter_subset,
exact set.subset.trans (set.inter_subset_inter_right _ h₂) h₃
end
theorem tendsto_iff_ptendsto (l₁ : filter α) (l₂ : filter β) (s : set α) (f : α → β) :
tendsto f (l₁ ⊓ 𝓟 s) l₂ ↔ ptendsto (pfun.res f s) l₁ l₂ :=
by simp only [tendsto, ptendsto, pmap_res]
theorem tendsto_iff_ptendsto_univ (l₁ : filter α) (l₂ : filter β) (f : α → β) :
tendsto f l₁ l₂ ↔ ptendsto (pfun.res f set.univ) l₁ l₂ :=
by { rw ← tendsto_iff_ptendsto, simp [principal_univ] }
def pcomap' (f : α →. β) (l : filter β) : filter α :=
filter.rcomap' f.graph' l
def ptendsto' (f : α →. β) (l₁ : filter α) (l₂ : filter β) := l₁ ≤ l₂.rcomap' f.graph'
theorem ptendsto'_def (f : α →. β) (l₁ : filter α) (l₂ : filter β) :
ptendsto' f l₁ l₂ ↔ ∀ s ∈ l₂, f.preimage s ∈ l₁ :=
rtendsto'_def _ _ _
theorem ptendsto_of_ptendsto' {f : α →. β} {l₁ : filter α} {l₂ : filter β} :
ptendsto' f l₁ l₂ → ptendsto f l₁ l₂ :=
begin
rw [ptendsto_def, ptendsto'_def],
assume h s sl₂,
exacts mem_sets_of_superset (h s sl₂) (pfun.preimage_subset_core _ _),
end
theorem ptendsto'_of_ptendsto {f : α →. β} {l₁ : filter α} {l₂ : filter β} (h : f.dom ∈ l₁) :
ptendsto f l₁ l₂ → ptendsto' f l₁ l₂ :=
begin
rw [ptendsto_def, ptendsto'_def],
assume h' s sl₂,
rw pfun.preimage_eq,
show pfun.core f s ∩ pfun.dom f ∈ l₁,
exact inter_mem_sets (h' s sl₂) h
end
end filter