feat(data/set): add some lemmas (#4263)

Some lemmas about sets, mostly involving disjointness
I also sneaked in the lemma `(λ x : α, y) = const α y` which is useful to rewrite with.

Author: fpvandoorn

src/data/set/basic.lean

@@ -1886,8 +1886,11 @@ by { split_ifs; simp [h] }
 theorem image_swap_eq_preimage_swap : image (@prod.swap α β) = preimage prod.swap :=
 image_eq_preimage_of_inverse prod.swap_left_inverse prod.swap_right_inverse
 
+theorem preimage_swap_prod {s : set α} {t : set β} : prod.swap ⁻¹' t.prod s = s.prod t :=
+by { ext ⟨x, y⟩, simp [and_comm] }
+
 theorem image_swap_prod : prod.swap '' t.prod s = s.prod t :=
-by { ext ⟨x, y⟩, simp [image_swap_eq_preimage_swap, and_comm] }
+by rw [image_swap_eq_preimage_swap, preimage_swap_prod]
 
 theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
   (image m₁ s).prod (image m₂ t) = image (λp:α×β, (m₁ p.1, m₂ p.2)) (s.prod t) :=

src/data/set/lattice.lean

@@ -1005,73 +1005,100 @@ end set
 
 /- disjoint sets -/
 
+section disjoint
+
+variables {s t u : set α}
+
+namespace disjoint
+
+/-! We define some lemmas in the `disjoint` namespace to be able to use projection notation. -/
+
+theorem union_left (hs : disjoint s u) (ht : disjoint t u) : disjoint (s ∪ t) u :=
+hs.sup_left ht
+
+theorem union_right (ht : disjoint s t) (hu : disjoint s u) : disjoint s (t ∪ u) :=
+ht.sup_right hu
+
+lemma preimage {α β} (f : α → β) {s t : set β} (h : disjoint s t) : disjoint (f ⁻¹' s) (f ⁻¹' t) :=
+λ x hx, h hx
+
+end disjoint
+
 namespace set
 
-protected theorem disjoint_iff {s t : set α} : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
+protected theorem disjoint_iff : disjoint s t ↔ s ∩ t ⊆ ∅ := iff.rfl
 
-theorem disjoint_iff_inter_eq_empty {s t : set α} : disjoint s t ↔ s ∩ t = ∅ :=
+theorem disjoint_iff_inter_eq_empty : disjoint s t ↔ s ∩ t = ∅ :=
 disjoint_iff
 
-lemma not_disjoint_iff {s t : set α} : ¬disjoint s t ↔ ∃x, x ∈ s ∧ x ∈ t :=
+lemma not_disjoint_iff : ¬disjoint s t ↔ ∃x, x ∈ s ∧ x ∈ t :=
 not_forall.trans $ exists_congr $ λ x, not_not
 
-lemma disjoint_left {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
+lemma disjoint_left : disjoint s t ↔ ∀ {a}, a ∈ s → a ∉ t :=
 show (∀ x, ¬(x ∈ s ∩ t)) ↔ _, from ⟨λ h a, not_and.1 $ h a, λ h a, not_and.2 $ h a⟩
 
-theorem disjoint_right {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
+theorem disjoint_right : disjoint s t ↔ ∀ {a}, a ∈ t → a ∉ s :=
 by rw [disjoint.comm, disjoint_left]
 
-theorem disjoint_of_subset_left {s t u : set α} (h : s ⊆ u) (d : disjoint u t) : disjoint s t :=
+theorem disjoint_of_subset_left (h : s ⊆ u) (d : disjoint u t) : disjoint s t :=
 d.mono_left h
 
-theorem disjoint_of_subset_right {s t u : set α} (h : t ⊆ u) (d : disjoint s u) : disjoint s t :=
+theorem disjoint_of_subset_right (h : t ⊆ u) (d : disjoint s u) : disjoint s t :=
 d.mono_right h
 
 theorem disjoint_of_subset {s t u v : set α} (h1 : s ⊆ u) (h2 : t ⊆ v) (d : disjoint u v) :
   disjoint s t :=
 d.mono h1 h2
 
-@[simp] theorem disjoint_union_left {s t u : set α} :
+@[simp] theorem disjoint_union_left :
   disjoint (s ∪ t) u ↔ disjoint s u ∧ disjoint t u :=
 disjoint_sup_left
 
-theorem disjoint.union_left {s t u : set α} (hs : disjoint s u) (ht : disjoint t u) :
-  disjoint (s ∪ t) u :=
-hs.sup_left ht
-
-@[simp] theorem disjoint_union_right {s t u : set α} :
+@[simp] theorem disjoint_union_right :
   disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u :=
 disjoint_sup_right
 
-theorem disjoint.union_right {s t u : set α} (ht : disjoint s t) (hu : disjoint s u) :
-  disjoint s (t ∪ u) :=
-ht.sup_right hu
-
 theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
 disjoint_iff.2 (inter_diff_self _ _)
 
 theorem disjoint_compl_left (s : set α) : disjoint sᶜ s := assume a ⟨h₁, h₂⟩, h₁ h₂
 
 theorem disjoint_compl_right (s : set α) : disjoint s sᶜ := assume a ⟨h₁, h₂⟩, h₂ h₁
 
-theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
+@[simp] lemma univ_disjoint {s : set α}: disjoint univ s ↔ s = ∅ :=
+by simp [set.disjoint_iff_inter_eq_empty]
+
+@[simp] lemma disjoint_univ {s : set α} : disjoint s univ ↔ s = ∅ :=
+by simp [set.disjoint_iff_inter_eq_empty]
+
+@[simp] theorem disjoint_singleton_left {a : α} {s : set α} : disjoint {a} s ↔ a ∉ s :=
 by simp [set.disjoint_iff, subset_def]; exact iff.rfl
 
-theorem disjoint_singleton_right {a : α} {s : set α} : disjoint s {a} ↔ a ∉ s :=
+@[simp] theorem disjoint_singleton_right {a : α} {s : set α} : disjoint s {a} ↔ a ∉ s :=
 by rw [disjoint.comm]; exact disjoint_singleton_left
 
 theorem disjoint_image_image {f : β → α} {g : γ → α} {s : set β} {t : set γ}
   (h : ∀b∈s, ∀c∈t, f b ≠ g c) : disjoint (f '' s) (g '' t) :=
 by rintros a ⟨⟨b, hb, eq⟩, ⟨c, hc, rfl⟩⟩; exact h b hb c hc eq
 
-lemma disjoint.preimage {α β} (f : α → β) {s t : set β} (h : disjoint s t) :
-  disjoint (f ⁻¹' s) (f ⁻¹' t) :=
-λ x hx, h hx
-
 theorem pairwise_on_disjoint_fiber (f : α → β) (s : set β) :
   pairwise_on s (disjoint on (λ y, f ⁻¹' {y})) :=
 λ y₁ _ y₂ _ hy x ⟨hx₁, hx₂⟩, hy (eq.trans (eq.symm hx₁) hx₂)
 
+lemma preimage_eq_empty {f : α → β} {s : set β} (h : disjoint s (range f)) :
+  f ⁻¹' s = ∅ :=
+by simpa using h.preimage f
+
+lemma preimage_eq_empty_iff {f : α → β} {s : set β} : disjoint s (range f) ↔ f ⁻¹' s = ∅ :=
+⟨preimage_eq_empty,
+  λ h, by { simp [eq_empty_iff_forall_not_mem, set.disjoint_iff_inter_eq_empty] at h ⊢, finish }⟩
+
+end set
+
+end disjoint
+
+namespace set
+
 /-- A collection of sets is `pairwise_disjoint`, if any two different sets in this collection
 are disjoint.  -/
 def pairwise_disjoint (s : set (set α)) : Prop :=
@@ -1088,7 +1115,7 @@ begin
   intro h, apply hxy, apply congr_arg f, exact subtype.eq h
 end
 
-/- warning: classical -/
+/- classical -/
 lemma pairwise_disjoint.elim {s : set (set α)} (h : pairwise_disjoint s) {x y : set α}
   (hx : x ∈ s) (hy : y ∈ s) (z : α) (hzx : z ∈ x) (hzy : z ∈ y) : x = y :=
 not_not.1 $ λ h', h x hx y hy h' ⟨hzx, hzy⟩

src/logic/function/basic.lean

@@ -26,6 +26,8 @@ variables {α β γ : Sort*} {f : α → β}
 lemma comp_apply {α : Sort u} {β : Sort v} {φ : Sort w} (f : β → φ) (g : α → β) (a : α) :
   (f ∘ g) a = f (g a) := rfl
 
+lemma const_def {y : β} : (λ x : α, y) = const α y := rfl
+
 @[simp] lemma const_apply {y : β} {x : α} : const α y x = y := rfl
 
 @[simp] lemma const_comp {f : α → β} {c : γ} : const β c ∘ f = const α c := rfl