feat(library/theories/move.lean): add facts to move in Lean 3

library/theories/move.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Temporary file; move in Lean3.
+-/
+import data.set algebra.order_bigops
+import data.finset data.list.sort
+
+-- move to data.set
+
+namespace set
+
+lemma inter_eq_self_of_subset {X : Type} {s t : set X} (Hst : s ⊆ t) : s ∩ t = s :=
+ext (take x, iff.intro
+  (assume H, !inter_subset_left H)
+  (assume H, and.intro H (Hst H)))
+
+lemma inter_eq_self_of_subset_right {X : Type} {s t : set X} (Hst : t ⊆ s) : s ∩ t = t :=
+by rewrite [inter_comm]; apply inter_eq_self_of_subset Hst
+
+proposition diff_self_inter {X : Type} (s t : set X) : s \ (s ∩ t) = s \ t :=
+by rewrite [*diff_eq, compl_inter, inter_distrib_left, inter_compl_self, empty_union]
+
+proposition diff_eq_diff {X : Type} {s t u : set X} (H : s ∩ u = s ∩ t) :
+  s \ u = s \ t :=
+by rewrite [-diff_self_inter, H, diff_self_inter]
+
+-- classical
+proposition inter_eq_inter_of_diff_eq_diff {X : Type} {s t u : set X} (H : s \ u = s \ t) :
+  s ∩ u = s ∩ t :=
+by rewrite [-compl_compl u, -compl_compl t]; apply diff_eq_diff H
+
+proposition compl_inter_eq_compl_inter {X : Type} {s t u : set X}
+    (H : u ∩ s = t ∩ s) :
+  -u ∩ s = -t ∩ s :=
+by rewrite [*inter_comm _ s]; apply diff_eq_diff; rewrite [*inter_comm s, H]
+
+proposition inter_eq_inter_of_compl_inter_eq_compl_inter {X : Type} {s t u : set X}
+    (H : -u ∩ s = -t ∩ s) :
+  u ∩ s = t ∩ s :=
+begin
+  rewrite [*inter_comm _ s], apply inter_eq_inter_of_diff_eq_diff,
+  rewrite [*diff_eq, *inter_comm s, H]
+end
+
+proposition singleton_subset_of_mem {X : Type} {x : X} {s : set X} (xs : x ∈ s) : '{x} ⊆ s :=
+take y, assume yx,
+  have y = x, from eq_of_mem_singleton yx,
+  by rewrite this; exact xs
+
+proposition mem_of_singleton_subset {X : Type} {x : X} {s : set X} (xs : '{x} ⊆ s) : x ∈ s :=
+xs !mem_singleton
+
+proposition singleton_subset_iff {X : Type} (x : X) (s : set X) : '{x} ⊆ s ↔ x ∈ s :=
+iff.intro mem_of_singleton_subset singleton_subset_of_mem
+
+lemma inter_eq_inter_left {X : Type} {s t u : set X} (H₁ : s ∩ t ⊆ u) (H₂ : s ∩ u ⊆ t) :
+  s ∩ t = s ∩ u :=
+eq_of_subset_of_subset
+  (subset_inter (inter_subset_left _ _) H₁)
+  (subset_inter (inter_subset_left _ _) H₂)
+
+lemma inter_eq_inter_right {X : Type} {s t u : set X} (H₁ : s ∩ t ⊆ u) (H₂ : u ∩ t ⊆ s) :
+  s ∩ t = u ∩ t :=
+eq_of_subset_of_subset
+  (subset_inter H₁ (inter_subset_right _ _))
+  (subset_inter H₂ (inter_subset_right _ _))
+
+proposition sUnion_subset {X : Type} {S : set (set X)} {t : set X} (H : ∀₀ u ∈ S, u ⊆ t) :
+  ⋃₀ S ⊆ t :=
+take x, assume Hx,
+obtain u [uS xu], from Hx,
+H uS xu
+
+proposition subset_of_sUnion_subset {X : Type} {S : set (set X)} {t : set X}
+  (H : ⋃₀ S ⊆ t) {u : set X} (Hu : u ∈ S) : u ⊆ t :=
+λ x xu, H (exists.intro u (and.intro Hu xu))
+
+proposition preimage_Union {I X Y : Type} (f : X → Y) (u : I → set Y) :
+  f '- (⋃ i, u i) = ⋃ i, (f '- (u i)) :=
+ext (take x, !iff.refl)
+
+lemma finite_sUnion {A : Type} {S : set (set A)} [H : finite S] :
+  (∀s, s ∈ S → finite s) → finite ⋃₀S :=
+induction_on_finite S
+  (by intro H; rewrite sUnion_empty; apply finite_empty)
+  (take a s, assume fins anins ih h,
+    begin
+      rewrite sUnion_insert,
+      apply finite_union,
+        {apply h _ (mem_insert a s)},
+      apply ih (forall_of_forall_insert h)
+    end)
+
+lemma subset_powerset_sUnion {A : Type} (S : set (set A)) : S ⊆ 𝒫 (⋃₀ S) :=
+take u, suppose u ∈ S, show u ⊆ ⋃₀ S, from subset_sUnion_of_mem this
+
+lemma finite_of_finite_sUnion {A : Type} (S : set (set A)) (H : finite ⋃₀S) : finite S :=
+have finite (𝒫 (⋃₀ S)), from finite_powerset _,
+show finite S, from finite_subset (subset_powerset_sUnion S)
+
+end set
+
+
+-- move to data.finset
+
+namespace finset
+
+section
+  variables {A : Type} [decidable_linear_order A]
+
+  definition finset_to_list (s : finset A) : list A :=
+  quot.lift_on s
+    (take l, list.sort le (subtype.elt_of l))
+    (take a b, assume eqab, list.sort_eq_of_perm eqab)
+
+  proposition to_finset_finset_to_list (s : finset A) : to_finset (finset_to_list s) = s :=
+  quot.induction_on s
+    begin
+      intro l,
+      have H : list.nodup (list.sort le (subtype.elt_of l)),
+        from perm.nodup_of_perm_of_nodup (perm.symm !list.sort_perm) (subtype.has_property l),
+      rewrite [↑finset_to_list, -to_finset_eq_of_nodup H],
+      apply quot.sound,
+      apply list.sort_perm
+    end
+
+  proposition nodup_finset_to_list (s : finset A) : list.nodup (finset_to_list s) :=
+  quot.induction_on s
+    (take l, perm.nodup_of_perm_of_nodup (perm.symm !list.sort_perm) (subtype.has_property l))
+
+  proposition sorted_finset_to_list (s : finset A) : list.sorted le (finset_to_list s) :=
+  quot.induction_on s
+    (take l, list.sorted_of_strongly_sorted (list.strongly_sorted_sort _))
+end
+
+end finset
+
+
+-- move to data.nat?
+
+namespace nat
+open finset
+
+theorem succ_Max₀_not_mem (s : finset ℕ) : succ (Max₀ s) ∉ s :=
+suppose succ (Max₀ s) ∈ s,
+have succ (Max₀ s) ≤ Max₀ s, from le_Max₀ this,
+show false, from not_succ_le_self this
+
+end nat

library/theories/topology/basic.lean

@@ -287,9 +287,10 @@ include Tm Tn
 definition continuous_at (f : M → N) (x : M) :=
   ∀ U : set N, f x ∈ U → Open U → ∃ V : set M, x ∈ V ∧ Open V ∧ f 'V ⊆ U
 
+/-
 definition continuous (f : M → N) :=
   ∀ x : M, continuous_at f x
-
+-/
 end continuity
 
 section boundary