Merge remote-tracking branch 'minchaowu/master'

analysis/real.lean

@@ -111,7 +111,7 @@ uniform_space.of_core { uniform_space.core .
   refl :=
     have ((λ (p : ℚ × ℚ), p.1 - p.2) '' id_rel) = {0},
       from set.subset.antisymm
-        (by simp [set.image_subset_iff_subset_preimage, subset_def, id_rel, -add_neg_eq_iff_eq_add] {contextual := tt})
+        (by simp [set.image_subset_iff, subset_def, id_rel, -add_neg_eq_iff_eq_add] {contextual := tt})
         (assume x hx, ⟨⟨0, 0⟩, begin revert hx, simp [*, id_rel, eq_comm] end⟩),
     by simp [le_vmap_iff_map_le, -sub_eq_add_neg, this]; exact pure_zero_le_zero_nhd,
   symm :=
@@ -861,7 +861,7 @@ have {r : ℝ | of_rat q < r} ⊆ closure (of_rat '' {x : ℚ | q ≤ x}),
       by simp [h₂.symm] at *; apply le_of_lt h₁,
 subset.antisymm
   (closure_minimal
-    (image_subset_iff_subset_preimage.mpr $ by simp [of_rat_le_of_rat] {contextual:=tt})
+    (image_subset_iff.mpr $ by simp [of_rat_le_of_rat] {contextual := tt})
     (is_closed_le continuous_const continuous_id)) $
   calc {r:ℝ | of_rat q ≤ r} ⊆ {of_rat q} ∪ {r | of_rat q < r} :
       assume x, by simp [le_iff_lt_or_eq, or_imp_distrib] {contextual := tt}
@@ -889,7 +889,7 @@ have hab : ({of_rat a, of_rat b}:set ℝ) ⊆ ivl,
   from subset.trans subset_closure $ closure_mono $
     by simp [subset_def, or_imp_distrib, forall_and_distrib, hab, le_refl],
 subset.antisymm
-  (closure_minimal (by simp [image_subset_iff_subset_preimage, of_rat_le_of_rat] {contextual := tt}) $
+  (closure_minimal (by simp [image_subset_iff, of_rat_le_of_rat] {contextual := tt}) $
     is_closed_inter (is_closed_le continuous_const continuous_id) (is_closed_le continuous_id continuous_const))
   (calc {r:ℝ | of_rat a ≤ r ∧ r ≤ of_rat b} ⊆ {of_rat a, of_rat b} ∪ (a_lt ∩ lt_b) :
       assume x, by simp [le_iff_lt_or_eq, and_imp, or_imp_distrib] {contextual := tt}

analysis/topology/continuity.lean

@@ -98,15 +98,15 @@ have ∀ (a : α), nhds a ⊓ principal s ≠ ⊥ → nhds (f a) ⊓ principal (
       (le_trans (map_mono inf_le_left) $ by rw [continuous_iff_tendsto] at h; exact h a)
       (le_trans (map_mono inf_le_right) $ by simp; exact subset.refl _),
   neq_bot_of_le_neq_bot h₁ h₂,
-by simp [image_subset_iff_subset_preimage, closure_eq_nhds]; assumption
+by simp [image_subset_iff, closure_eq_nhds]; assumption
 
 lemma compact_image {s : set α} {f : α → β} (hs : compact s) (hf : continuous f) : compact (f '' s) :=
 compact_of_finite_subcover $ assume c hco hcs,
   have hdo : ∀t∈c, is_open (preimage f t), from assume t' ht, hf _ $ hco _ ht,
   have hds : s ⊆ ⋃i∈c, preimage f i,
     by simpa [subset_def, -mem_image] using hcs,
   let ⟨d', hcd', hfd', hd'⟩ := compact_elim_finite_subcover_image hs hdo hds in
-  ⟨d', hcd', hfd', by simpa [subset_def, -mem_image, image_subset_iff_subset_preimage] using hd'⟩
+  ⟨d', hcd', hfd', by simpa [subset_def, -mem_image, image_subset_iff] using hd'⟩
 
 end
 
@@ -658,7 +658,7 @@ let ⟨s'', hs''₁, hs''₂, hs''₃⟩ := nhds_is_closed hs in
 let ⟨s', hs'₁, (hs'₂ : preimage e s' ⊆ preimage f s'')⟩ := mem_of_nhds hφ hs''₁ in
 let ⟨t, (ht₁ : t ⊆ φ ∩ s'), ht₂, ht₃⟩ := mem_nhds_sets_iff.mp $ inter_mem_sets hφ hs'₁ in
 have h₁ : closure (f '' preimage e s') ⊆ s'',
-  by rw [closure_subset_iff_subset_of_is_closed hs''₃, image_subset_iff_subset_preimage]; exact hs'₂,
+  by rw [closure_subset_iff_subset_of_is_closed hs''₃, image_subset_iff]; exact hs'₂,
 have h₂ : t ⊆ preimage (de.ext f) (closure (f '' preimage e t)), from
   assume b' hb',
   have nhds b' ≤ principal t, by simp; exact mem_nhds_sets ht₂ hb',
@@ -732,7 +732,7 @@ lemma is_closed_property [topological_space α] [topological_space β] {e : α 
   ∀b, p b :=
 have univ ⊆ {b | p b},
   from calc univ = closure (e '' univ) : he.symm
-    ... ⊆ closure {b | p b} : closure_mono $ image_subset_iff_subset_preimage.mpr $ assume a _, h a
+    ... ⊆ closure {b | p b} : closure_mono $ image_subset_iff.mpr $ assume a _, h a
     ... = _ : closure_eq_of_is_closed hp,
 assume b, this trivial
 
@@ -756,7 +756,7 @@ lemma mem_closure_of_continuous [topological_space α] [topological_space β]
   f a ∈ closure t :=
 calc f a ∈ f '' closure s : mem_image_of_mem _ ha
   ... ⊆ closure (f '' s) : image_closure_subset_closure_image hf
-  ... ⊆ closure (closure t) : closure_mono $ image_subset_iff_subset_preimage.mpr $ h
+  ... ⊆ closure (closure t) : closure_mono $ image_subset_iff.mpr $ h
   ... ⊆ closure t : begin rw [closure_eq_of_is_closed], exact subset.refl _, exact is_closed_closure end
 
 lemma mem_closure_of_continuous2 [topological_space α] [topological_space β] [topological_space γ]

analysis/topology/infinite_sum.lean

@@ -165,7 +165,7 @@ suffices at_top.map (λs:finset β, s.sum f) ≤ at_top.map (λs:finset γ, s.su
   from le_trans this hf,
 by rw [map_at_top_eq, map_at_top_eq];
 from (le_infi $ assume b, let ⟨v, hv⟩ := h_eq b in infi_le_of_le v $
-  by simp [image_subset_iff_subset_preimage]; exact hv)
+  by simp [image_subset_iff]; exact hv)
 
 lemma is_sum_iff_is_sum
   (h₁ : ∀u:finset γ, ∃v:finset β, ∀v', v ⊆ v' → ∃u', u ⊆ u' ∧ u'.sum g = v'.sum f)

analysis/topology/uniform_space.lean

@@ -658,7 +658,7 @@ have {p:α×α | (f p.1, f p.2) ∈ t} ∈ (@uniformity α _).sets,
 let ⟨c, hfc, hct⟩ := hs _ this in
 ⟨f '' c, finite_image hfc,
   begin
-    simp [image_subset_iff_subset_preimage],
+    simp [image_subset_iff],
     simp [subset_def] at hct,
     intros x hx, simp [-mem_image],
     exact let ⟨i, hi, ht⟩ := hct x hx in ⟨f i, mem_image_of_mem f hi, ht⟩
@@ -991,7 +991,7 @@ show preimage (λp:(α×α), (ψ p.1, ψ p.2)) d ∈ uniformity.sets,
     from calc set.prod (f '' preimage e m₁) (f '' preimage e m₂) =
       (λp:(β×β), (f p.1, f p.2)) '' (set.prod (preimage e m₁) (preimage e m₂)) : prod_image_image_eq
     ... ⊆ (λp:(β×β), (f p.1, f p.2)) '' preimage (λp:(β×β), (f p.1, f p.2)) s : mono_image this
-    ... ⊆ s : image_subset_iff_subset_preimage.mpr $ subset.refl _,
+    ... ⊆ s : image_subset_iff.mpr $ subset.refl _,
   have (a, b) ∈ s, from @this (a, b) ⟨ha₁, hb₁⟩,
   hs_comp $ show (ψ x₁, ψ x₂) ∈ comp_rel s (comp_rel s s),
     from ⟨a, ha₂, ⟨b, this, hb₂⟩⟩

data/set/basic.lean

@@ -507,6 +507,9 @@ assume x hx, h hx
 
 @[simp] theorem preimage_compl {s : set β} : f ⁻¹' (- s) = - (f ⁻¹' s) := rfl
 
+@[simp] theorem preimage_diff (f : α → β) (s t : set β) :
+  f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t := rfl
+
 @[simp] theorem preimage_set_of_eq {p : α → Prop} {f : β → α} : f ⁻¹' {a | p a} = {a | p (f a)} :=
 rfl
 
@@ -644,14 +647,13 @@ theorem mem_image_iff_of_inverse {f : α → β} {g : β → α} {b : β} {s : s
 by rw image_eq_preimage_of_inverse h₁ h₂; refl
 
 /- image and preimage are a Galois connection -/
-theorem image_subset_iff_subset_preimage {s : set α} {t : set β} {f : α → β} :
+theorem image_subset_iff {s : set α} {t : set β} {f : α → β} :
   f '' s ⊆ t ↔ s ⊆ f ⁻¹' t :=
-⟨assume h x hx, h (mem_image_of_mem f hx),
- assume h x hx, match x, hx with ._, ⟨y, hy, rfl⟩ := h hy end⟩
+ball_image_iff
 
 theorem image_preimage_subset (f : α → β) (s : set β) :
   f '' (f ⁻¹' s) ⊆ s :=
-image_subset_iff_subset_preimage.2 (subset.refl _)
+image_subset_iff.2 (subset.refl _)
 
 theorem subset_preimage_image (f : α → β) (s : set α) :
   s ⊆ f ⁻¹' (f '' s) :=
@@ -682,6 +684,18 @@ lemma compl_image_set_of {α : Type u} {p : set α → Prop} :
   compl '' {x | p x} = {x | p (- x)} :=
 congr_fun compl_image p
 
+theorem inter_preimage_subset (s : set α) (t : set β) (f : α → β) :
+  s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t) :=
+λ x h, ⟨mem_image_of_mem _ h.left, h.right⟩
+
+theorem union_preimage_subset (s : set α) (t : set β) (f : α → β) :
+  s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t) :=
+λ x h, or.elim h (λ l, or.inl $ mem_image_of_mem _ l) (λ r, or.inr r)
+
+theorem subset_image_union (f : α → β) (s : set α) (t : set β) :
+  f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t :=
+image_subset_iff.2 (union_preimage_subset _ _ _)
+
 end image
 
 lemma univ_eq_true_false : univ = ({true, false} : set Prop) :=

data/set/function.lean

@@ -0,0 +1,227 @@
+/-
+Copyright (c) 2014 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad, Andrew Zipperer, Haitao Zhang, Minchao Wu
+
+Functions over sets.
+-/
+import data.set.basic
+open function
+
+namespace set
+universes u v w x
+variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x}
+
+/- maps to -/
+
+@[reducible] def maps_to (f : α → β) (a : set α) (b : set β) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b
+
+theorem maps_to_of_eq_on {f1 f2 : α → β} {a : set α} {b : set β} (h₁ : eq_on f1 f2 a)
+    (h₂ : maps_to f1 a b) :
+  maps_to f2 a b :=
+λ x h, by rw [← h₁ _ h]; exact h₂ h
+
+theorem maps_to_comp {g : β → γ} {f : α → β} {a : set α} {b : set β} {c : set γ}
+   (h₁ : maps_to g b c) (h₂ : maps_to f a b) : maps_to (g ∘ f) a c :=
+λ x h, h₁ (h₂ h)
+
+theorem maps_to_univ_univ (f : α → β) : maps_to f univ univ :=
+λ x h, trivial
+
+theorem image_subset_of_maps_to_of_subset {f : α → β} {a c : set α} {b : set β} (h₁ : maps_to f a b)
+  (h₂ : c ⊆ a) :
+  f '' c ⊆ b :=
+λ y hy, let ⟨x, hx, heq⟩ := hy in 
+by rw [←heq]; apply h₁; apply h₂; assumption
+
+theorem image_subset_of_maps_to {f : α → β} {a : set α} {b : set β} (h : maps_to f a b) :
+  f '' a ⊆ b :=
+image_subset_of_maps_to_of_subset h (subset.refl _)
+
+/- injectivity -/
+
+@[reducible] def inj_on (f : α → β) (a : set α) : Prop :=
+∀⦃x1 x2 : α⦄, x1 ∈ a → x2 ∈ a → f x1 = f x2 → x1 = x2
+
+theorem inj_on_empty (f : α → β) : inj_on f ∅ :=
+λ _ _ h₁ _ _, false.elim h₁
+
+theorem inj_on_of_eq_on {f1 f2 : α → β} {a : set α} (h₁ : eq_on f1 f2 a)
+    (h₂ : inj_on f1 a) :
+  inj_on f2 a :=
+λ _ _ h₁' h₂' heq, by apply h₂ h₁' h₂'; rw [h₁, heq, ←h₁]; repeat {assumption}
+
+theorem inj_on_comp {g : β → γ} {f : α → β} {a : set α} {b : set β}
+    (h₁ : maps_to f a b) (h₂ : inj_on g b) (h₃: inj_on f a) :
+  inj_on (g ∘ f) a :=
+λ _ _ h₁' h₂' heq, 
+by apply h₃ h₁' h₂'; apply h₂; repeat {apply h₁, assumption}; assumption
+
+theorem inj_on_of_inj_on_of_subset {f : α → β} {a b : set α} (h₁ : inj_on f b) (h₂ : a ⊆ b) :
+  inj_on f a :=
+λ _ _ h₁' h₂' heq, h₁ (h₂ h₁') (h₂ h₂') heq
+
+lemma injective_iff_inj_on_univ {f : α → β} : injective f ↔ inj_on f univ :=
+iff.intro (λ h _ _ _ _ heq, h heq) (λ h _ _ heq, h trivial trivial heq)
+
+/- surjectivity -/
+
+@[reducible] def surj_on (f : α → β) (a : set α) (b : set β) : Prop := b ⊆ f '' a
+
+theorem surj_on_of_eq_on {f1 f2 : α → β} {a : set α} {b : set β} (h₁ : eq_on f1 f2 a)
+    (h₂ : surj_on f1 a b) :
+  surj_on f2 a b :=
+λ _ h, let ⟨x, hx⟩ := h₂ h in 
+⟨x, hx.left, by rw [←h₁ _ hx.left]; exact hx.right⟩
+
+theorem surj_on_comp {g : β → γ} {f : α → β} {a : set α} {b : set β} {c : set γ}
+  (h₁ : surj_on g b c) (h₂ : surj_on f a b) :
+  surj_on (g ∘ f) a c :=
+λ z h, let ⟨y, hy⟩ := h₁ h, ⟨x, hx⟩ := h₂ hy.left in
+       ⟨x, hx.left, calc g (f x) = g y : by rw [hx.right]
+                          ...    = z   : hy.right⟩
+
+lemma surjective_iff_surj_on_univ {f : α → β} : surjective f ↔ surj_on f univ univ :=
+by simp [surjective, surj_on, subset_def]
+
+lemma image_eq_of_maps_to_of_surj_on {f : α → β} {a : set α} {b : set β}
+    (h₁ : maps_to f a b) (h₂ : surj_on f a b) :
+  f '' a = b :=
+eq_of_subset_of_subset (image_subset_of_maps_to h₁) h₂
+
+/- bijectivity -/
+
+@[reducible] def bij_on (f : α → β) (a : set α) (b : set β) : Prop :=
+maps_to f a b ∧ inj_on f a ∧ surj_on f a b
+
+lemma maps_to_of_bij_on {f : α → β} {a : set α} {b : set β} (h : bij_on f a b) :
+      maps_to f a b :=
+h.left
+
+lemma inj_on_of_bij_on {f : α → β} {a : set α} {b : set β} (h : bij_on f a b) :
+      inj_on f a :=
+h.right.left
+
+lemma surj_on_of_bij_on {f : α → β} {a : set α} {b : set β} (h : bij_on f a b) :
+      surj_on f a b :=
+h.right.right
+
+lemma bij_on.mk {f : α → β} {a : set α} {b : set β}
+                (h₁ : maps_to f a b) (h₂ : inj_on f a) (h₃ : surj_on f a b) :
+      bij_on f a b :=
+⟨h₁, h₂, h₃⟩
+
+theorem bij_on_of_eq_on {f1 f2 : α → β} {a : set α} {b : set β} (h₁ : eq_on f1 f2 a)
+     (h₂ : bij_on f1 a b) : bij_on f2 a b :=
+let ⟨map, inj, surj⟩ := h₂ in 
+⟨maps_to_of_eq_on h₁ map, inj_on_of_eq_on h₁ inj, surj_on_of_eq_on h₁ surj⟩
+
+lemma image_eq_of_bij_on {f : α → β} {a : set α} {b : set β} (h : bij_on f a b) :
+  f '' a = b :=
+image_eq_of_maps_to_of_surj_on h.left h.right.right
+
+theorem bij_on_comp {g : β → γ} {f : α → β} {a : set α} {b : set β} {c : set γ}
+  (h₁ : bij_on g b c) (h₂: bij_on f a b) :
+  bij_on (g ∘ f) a c :=
+let ⟨gmap, ginj, gsurj⟩ := h₁, ⟨fmap, finj, fsurj⟩ := h₂ in
+⟨maps_to_comp gmap fmap, inj_on_comp fmap ginj finj, surj_on_comp gsurj fsurj⟩
+
+lemma bijective_iff_bij_on_univ {f : α → β} : bijective f ↔ bij_on f univ univ :=
+iff.intro 
+(λ h, let ⟨inj, surj⟩ := h in 
+⟨maps_to_univ_univ f, iff.mp injective_iff_inj_on_univ inj, iff.mp surjective_iff_surj_on_univ surj⟩)
+(λ h, let ⟨map, inj, surj⟩ := h in 
+⟨iff.mpr injective_iff_inj_on_univ inj, iff.mpr surjective_iff_surj_on_univ surj⟩)
+
+/- left inverse -/
+
+-- g is a left inverse to f on a
+@[reducible] def left_inv_on (g : β → α) (f : α → β) (a : set α) : Prop :=
+∀ x ∈ a, g (f x) = x
+
+theorem left_inv_on_of_eq_on_left {g1 g2 : β → α} {f : α → β} {a : set α} {b : set β}
+  (h₁ : maps_to f a b) (h₂ : eq_on g1 g2 b) (h₃ : left_inv_on g1 f a) : left_inv_on g2 f a :=
+λ x h,
+calc
+  g2 (f x) = g1 (f x) : eq.symm $ h₂ _ (h₁ h)
+       ... = x        : h₃ _ h
+
+theorem left_inv_on_of_eq_on_right {g : β → α} {f1 f2 : α → β} {a : set α}
+  (h₁ : eq_on f1 f2 a) (h₂ : left_inv_on g f1 a) : left_inv_on g f2 a :=
+λ x h, 
+calc
+  g (f2 x) = g (f1 x) : congr_arg g (h₁ _ h).symm
+       ... = x        : h₂ _ h
+
+theorem inj_on_of_left_inv_on {g : β → α} {f : α → β} {a : set α} (h : left_inv_on g f a) :
+  inj_on f a :=
+λ x₁ x₂ h₁ h₂ heq, 
+calc
+  x₁    = g (f x₁) : eq.symm $ h _ h₁
+  ...   = g (f x₂) : congr_arg g heq
+  ...   = x₂       : h _ h₂
+
+theorem left_inv_on_comp {f' : β → α} {g' : γ → β} {g : β → γ} {f : α → β}
+   {a : set α} {b : set β} (h₁ : maps_to f a b)
+    (h₂ : left_inv_on f' f a) (h₃ : left_inv_on g' g b) : left_inv_on (f' ∘ g') (g ∘ f) a :=
+λ x h,
+calc
+  (f' ∘ g') ((g ∘ f) x) = f' (f x) : congr_arg f' (h₃ _ (h₁ h))
+  ...                   = x        : h₂ _ h
+
+/- right inverse -/
+
+-- g is a right inverse to f on a
+@[reducible] def right_inv_on (g : β → α) (f : α → β) (b : set β) : Prop :=
+left_inv_on f g b
+
+theorem right_inv_on_of_eq_on_left {g1 g2 : β → α} {f : α → β} {a : set α} {b : set β}
+  (h₁ : eq_on g1 g2 b) (h₂ : right_inv_on g1 f b) : right_inv_on g2 f b :=
+left_inv_on_of_eq_on_right h₁ h₂
+
+theorem right_inv_on_of_eq_on_right {g : β → α} {f1 f2 : α → β} {a : set α} {b : set β}
+  (h₁ : maps_to g b a) (h₂ : eq_on f1 f2 a) (h₃ : right_inv_on g f1 b) : right_inv_on g f2 b :=
+left_inv_on_of_eq_on_left h₁ h₂ h₃
+
+theorem surj_on_of_right_inv_on {g : β → α} {f : α → β} {a : set α} {b : set β}
+    (h₁ : maps_to g b a) (h₂ : right_inv_on g f b) :
+  surj_on f a b :=
+λ y h, ⟨g y, h₁ h, h₂ _ h⟩
+
+theorem right_inv_on_comp {f' : β → α} {g' : γ → β} {g : β → γ} {f : α → β}
+   {c : set γ} {b : set β} (g'cb : maps_to g' c b)
+    (h₁ : right_inv_on f' f b) (h₂ : right_inv_on g' g c) : right_inv_on (f' ∘ g') (g ∘ f) c :=
+left_inv_on_comp g'cb h₂ h₁
+
+theorem right_inv_on_of_inj_on_of_left_inv_on {f : α → β} {g : β → α} {a : set α} {b : set β}
+    (h₁ : maps_to f a b) (h₂ : maps_to g b a) (h₃ : inj_on f a) (h₄ : left_inv_on f g b) :
+  right_inv_on f g a :=
+λ x h, h₃ (h₂ $ h₁ h) h (h₄ _ (h₁ h))
+
+theorem eq_on_of_left_inv_of_right_inv {g₁ g₂ : β → α} {f : α → β} {a : set α} {b : set β}
+  (h₁ : maps_to g₂ b a) (h₂ : left_inv_on g₁ f a) (h₃ : right_inv_on g₂ f b) : eq_on g₁ g₂ b :=
+λ y h, 
+calc
+  g₁ y = (g₁ ∘ f ∘ g₂) y : congr_arg g₁ (h₃ _ h).symm
+  ...  = g₂ y            : h₂ _ (h₁ h) 
+
+theorem left_inv_on_of_surj_on_right_inv_on {f : α → β} {g : β → α} {a : set α} {b : set β}
+    (h₁ : surj_on f a b) (h₂ : right_inv_on f g a) :
+  left_inv_on f g b :=
+λ y h, let ⟨x, hx, heq⟩ := h₁ h in
+calc
+  (f ∘ g) y = (f ∘ g ∘ f) x : congr_arg (f ∘ g) heq.symm
+  ...     = f x             : congr_arg f (h₂ _ hx)
+  ...     = y               : heq
+
+/- inverses -/
+
+-- g is an inverse to f viewed as a map from a to b
+@[reducible] def inv_on (g : β → α) (f : α → β) (a : set α) (b : set β) : Prop :=
+left_inv_on g f a ∧ right_inv_on g f b
+
+theorem bij_on_of_inv_on {g : β → α} {f : α → β} {a : set α} {b : set β} (h₁ : maps_to f a b)
+  (h₂ : maps_to g b a) (h₃ : inv_on g f a b) : bij_on f a b :=
+⟨h₁, inj_on_of_left_inv_on h₃.left, surj_on_of_right_inv_on h₂ h₃.right⟩
+
+end set