feat(data/set/finite): finite_subset_Union, disjoint_mono

Author: digama0

data/set/finite.lean

@@ -181,6 +181,9 @@ fintype_of_finset (s.to_finset.image f) $ by simp
 instance fintype_range [decidable_eq β] (f : α → β) [fintype α] : fintype (range f) :=
 fintype_of_finset (finset.univ.image f) $ by simp [range]
 
+theorem finite_range (f : α → β) [fintype α] : finite (range f) :=
+by haveI := classical.dec_eq β; exact ⟨by apply_instance⟩
+
 theorem finite_image {s : set α} (f : α → β) : finite s → finite (f '' s)
 | ⟨h⟩ := ⟨@set.fintype_image _ _ (classical.dec_eq β) _ _ h⟩
 
@@ -252,6 +255,16 @@ end finset
 
 namespace set
 
+lemma finite_subset_Union {s : set α} (hs : finite s)
+  {ι} {t : ι → set α} (h : s ⊆ ⋃ i, t i) : ∃ I : set ι, finite I ∧ s ⊆ ⋃ i ∈ I, t i :=
+begin
+  unfreezeI, cases hs,
+  have : ∀ x : s, ∃ i, x.1 ∈ t i, {simpa [subset_def] using h},
+  cases classical.axiom_of_choice this with f hf,
+  refine ⟨range f, finite_range f, _⟩,
+  rintro x hx, simp, exact ⟨_, ⟨_, hx, rfl⟩, hf ⟨x, hx⟩⟩
+end
+
 lemma infinite_univ_nat : infinite (univ : set ℕ) :=
 assume (h : finite (univ : set ℕ)),
 let ⟨n, hn⟩ := finset.exists_nat_subset_range h.to_finset in

data/set/lattice.lean

@@ -561,6 +561,15 @@ disjoint.comm.1
 theorem disjoint_bot_left {a : α} : disjoint ⊥ a := disjoint_iff.2 bot_inf_eq
 theorem disjoint_bot_right {a : α} : disjoint a ⊥ := disjoint_iff.2 inf_bot_eq
 
+theorem disjoint_mono {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
+  disjoint b d → disjoint a c := le_trans (inf_le_inf h₁ h₂)
+
+theorem disjoint_mono_left {a b c : α} (h : a ≤ b) : disjoint b c → disjoint a c :=
+disjoint_mono h (le_refl _)
+
+theorem disjoint_mono_right {a b c : α} (h : b ≤ c) : disjoint a c → disjoint a b :=
+disjoint_mono (le_refl _) h
+
 end disjoint
 
 theorem set.disjoint_diff {a b : set α} : disjoint a (b \ a) :=