feat(data/set/lattice): add lemmas disjoint.union_left/right etc (#…

…3554)

src/data/set/lattice.lean

@@ -824,7 +824,7 @@ theorem disjoint_iff_inter_eq_empty {s t : set α} : disjoint s t ↔ s ∩ t =
 disjoint_iff
 
 lemma not_disjoint_iff {s t : set α} : ¬disjoint s t ↔ ∃x, x ∈ s ∧ x ∈ t :=
-(not_congr (set.disjoint_iff.trans subset_empty_iff)).trans ne_empty_iff_nonempty
+classical.not_forall.trans $ exists_congr $ λ x, classical.not_not
 
 lemma disjoint_left {s t : set α} : 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⟩
@@ -833,14 +833,30 @@ theorem disjoint_right {s t : set α} : disjoint s t ↔ ∀ {a}, a ∈ t → a
 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 :=
-disjoint_left.2 (λ x m₁, (disjoint_left.1 d) (h m₁))
+d.mono_left h
 
 theorem disjoint_of_subset_right {s t u : set α} (h : t ⊆ u) (d : disjoint s u) : disjoint s t :=
-disjoint_right.2 (λ x m₁, (disjoint_right.1 d) (h m₁))
+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 :=
-disjoint_of_subset_left h1 $ disjoint_of_subset_right h2 d
+d.mono h1 h2
+
+@[simp] theorem disjoint_union_left {s t u : set α} :
+  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 α} :
+  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 _ _)

src/order/bounded_lattice.lean

@@ -898,6 +898,9 @@ instance [bounded_distrib_lattice α] [bounded_distrib_lattice β] :
 end prod
 
 section disjoint
+
+section semilattice_inf_bot
+
 variable [semilattice_inf_bot α]
 
 /-- Two elements of a lattice are disjoint if their inf is the bottom element.
@@ -934,6 +937,26 @@ by simp [disjoint]
 lemma disjoint.ne {a b : α} (ha : a ≠ ⊥) (hab : disjoint a b) : a ≠ b :=
 by { intro h, rw [←h, disjoint_self] at hab, exact ha hab }
 
+end semilattice_inf_bot
+
+section bounded_distrib_lattice
+
+variables [bounded_distrib_lattice α] {a b c : α}
+
+@[simp] lemma disjoint_sup_left : disjoint (a ⊔ b) c ↔ disjoint a c ∧ disjoint b c :=
+by simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]
+
+@[simp] lemma disjoint_sup_right : disjoint a (b ⊔ c) ↔ disjoint a b ∧ disjoint a c :=
+by simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]
+
+lemma disjoint.sup_left (ha : disjoint a c) (hb : disjoint b c) : disjoint (a ⊔ b) c :=
+disjoint_sup_left.2 ⟨ha, hb⟩
+
+lemma disjoint.sup_right (hb : disjoint a b) (hc : disjoint a c) : disjoint a (b ⊔ c) :=
+disjoint_sup_right.2 ⟨hb, hc⟩
+
+end bounded_distrib_lattice
+
 end disjoint
 
 /-!