feat(library/data/finset): define intersection for finsets

library/data/finset/basic.lean

@@ -231,4 +231,53 @@ theorem empty_union (s : finset A) : ∅ ∪ s = s :=
 calc ∅ ∪ s = s ∪ ∅ : union.comm
        ... = s     : union_empty
 end union
+
+/- intersection -/
+section intersection
+variable [h : decidable_eq A]
+include h
+
+definition intersection (s₁ s₂ : finset A) : finset A :=
+quot.lift_on₂ s₁ s₂
+  (λ l₁ l₂,
+    to_finset_of_nodup (list.intersection (elt_of l₁) (elt_of l₂))
+                       (nodup_intersection_of_nodup _ (has_property l₁)))
+  (λ v₁ v₂ w₁ w₂ p₁ p₂, quot.sound (perm_intersection p₁ p₂))
+
+notation s₁ ∩ s₂ := intersection s₁ s₂
+
+theorem mem_of_mem_intersection_left {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₁ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_left ainl₁l₂)
+
+theorem mem_of_mem_intersection_right {a : A} {s₁ s₂ : finset A} : a ∈ s₁ ∩ s₂ → a ∈ s₂ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁l₂, list.mem_of_mem_intersection_right ainl₁l₂)
+
+theorem mem_intersection_of_mem_of_mem {a : A} {s₁ s₂ : finset A} : a ∈ s₁ → a ∈ s₂ → a ∈ s₁ ∩ s₂ :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ ainl₁ ainl₂, list.mem_intersection_of_mem_of_mem ainl₁ ainl₂)
+
+theorem mem_intersection_eq (a : A) (s₁ s₂ : finset A) : (a ∈ s₁ ∩ s₂) = (a ∈ s₁ ∧ a ∈ s₂) :=
+propext (iff.intro
+ (λ h, and.intro (mem_of_mem_intersection_left h) (mem_of_mem_intersection_right h))
+ (λ h, mem_intersection_of_mem_of_mem (and.elim_left h) (and.elim_right h)))
+
+theorem intersection.comm (s₁ s₂ : finset A) : s₁ ∩ s₂ = s₂ ∩ s₁ :=
+ext (λ a, by rewrite [*mem_intersection_eq]; exact and.comm)
+
+theorem intersection.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
+ext (λ a, by rewrite [*mem_intersection_eq]; exact and.assoc)
+
+theorem intersection_self (s : finset A) : s ∩ s = s :=
+ext (λ a, iff.intro
+  (λ h, mem_of_mem_intersection_right h)
+  (λ h, mem_intersection_of_mem_of_mem h h))
+
+theorem intersection_empty (s : finset A) : s ∩ ∅ = ∅ :=
+ext (λ a, iff.intro
+  (λ h : a ∈ s ∩ ∅, absurd (mem_of_mem_intersection_right h) !not_mem_empty)
+  (λ h : a ∈ ∅,     absurd h !not_mem_empty))
+
+theorem empty_intersection (s : finset A) : ∅ ∩ s = ∅ :=
+calc ∅ ∩ s = s ∩ ∅ : intersection.comm
+       ... = ∅     : intersection_empty
+end intersection
 end finset

library/data/list/set.lean

@@ -585,7 +585,7 @@ theorem mem_of_mem_intersection_right : ∀ {l₁ l₂} {a : A}, a ∈ intersect
   (λ nbinl₂ : b ∉ l₂,
     by rewrite [intersection_cons_of_not_mem _ nbinl₂ at i]; exact (mem_of_mem_intersection_right i))
 
-theorem mem_intersection_of_mem_of_men : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ intersection l₁ l₂
+theorem mem_intersection_of_mem_of_mem : ∀ {l₁ l₂} {a : A}, a ∈ l₁ → a ∈ l₂ → a ∈ intersection l₁ l₂
 | []      l₂ a i₁ i₂ := absurd i₁ !not_mem_nil
 | (b::l₁) l₂ a i₁ i₂ := by_cases
   (λ binl₂  : b ∈ l₂,
@@ -595,12 +595,12 @@ theorem mem_intersection_of_mem_of_men : ∀ {l₁ l₂} {a : A}, a ∈ l₁ →
      (λ ainl₁ : a ∈ l₁,
         by rewrite [intersection_cons_of_mem _ binl₂];
            apply mem_cons_of_mem;
-           exact (mem_intersection_of_mem_of_men ainl₁ i₂)))
+           exact (mem_intersection_of_mem_of_mem ainl₁ i₂)))
   (λ nbinl₂ : b ∉ l₂,
     or.elim (eq_or_mem_of_mem_cons i₁)
      (λ aeqb  : a = b, absurd (aeqb ▸ i₂) nbinl₂)
      (λ ainl₁ : a ∈ l₁,
-       by rewrite [intersection_cons_of_not_mem _ nbinl₂]; exact (mem_intersection_of_mem_of_men ainl₁ i₂)))
+       by rewrite [intersection_cons_of_not_mem _ nbinl₂]; exact (mem_intersection_of_mem_of_mem ainl₁ i₂)))
 
 theorem nodup_intersection_of_nodup : ∀ {l₁ : list A} (l₂), nodup l₁ → nodup (intersection l₁ l₂)
 | []      l₂ d := nodup_nil