feat(data/set): more lemmas (#6474)

src/data/set/finite.lean

@@ -176,6 +176,9 @@ fintype.card_of_subsingleton _
 @[simp] theorem finite_singleton (a : α) : finite ({a} : set α) :=
 ⟨set.fintype_singleton _⟩
 
+lemma subsingleton.finite {s : set α} (h : s.subsingleton) : finite s :=
+h.induction_on finite_empty finite_singleton
+
 instance fintype_pure : ∀ a : α, fintype (pure a : set α) :=
 set.fintype_singleton
 
@@ -335,6 +338,11 @@ finite_of_finite_image I (h.subset (image_preimage_subset f s))
 theorem finite.preimage_embedding {s : set β} (f : α ↪ β) (h : s.finite) : (f ⁻¹' s).finite :=
 finite.preimage (λ _ _ _ _ h', f.injective h') h
 
+lemma finite_option {s : set (option α)} : finite s ↔ finite {x : α | some x ∈ s} :=
+⟨λ h, h.preimage_embedding embedding.some,
+  λ h, ((h.image some).union (finite_singleton none)).subset $
+    λ x, option.cases_on x (λ _, or.inr rfl) (λ x hx, or.inl $ mem_image_of_mem _ hx)⟩
+
 instance fintype_Union [decidable_eq α] {ι : Type*} [fintype ι]
   (f : ι → set α) [∀ i, fintype (f i)] : fintype (⋃ i, f i) :=
 fintype.of_finset (finset.univ.bUnion (λ i, (f i).to_finset)) $ by simp

src/data/set/lattice.lean

@@ -132,11 +132,9 @@ set.subset_Inter $ λ j, let ⟨i, hi⟩ := h j in Inter_subset_of_subset i hi
 lemma Inter_set_of (P : ι → α → Prop) : (⋂ i, {x : α | P i x }) = {x : α | ∀ i, P i x} :=
 by { ext, simp }
 
-theorem Union_const [nonempty ι] (s : set β) : (⋃ i:ι, s) = s :=
-ext $ by simp
+theorem Union_const [nonempty ι] (s : set β) : (⋃ i:ι, s) = s := supr_const
 
-theorem Inter_const [nonempty ι] (s : set β) : (⋂ i:ι, s) = s :=
-ext $ by simp
+theorem Inter_const [nonempty ι] (s : set β) : (⋂ i:ι, s) = s := infi_const
 
 @[simp] -- complete_boolean_algebra
 theorem compl_Union (s : ι → set β) : (⋃ i, s i)ᶜ = (⋂ i, (s i)ᶜ) :=
@@ -226,7 +224,13 @@ end
 lemma Union_Inter_subset {ι ι' α} {s : ι → ι' → set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j :=
 by { rintro x ⟨_, ⟨i, rfl⟩, hx⟩ _ ⟨j, rfl⟩, exact ⟨_, ⟨i, rfl⟩, hx _ ⟨j, rfl⟩⟩ }
 
-/- bounded unions and intersections -/
+lemma Union_option {ι} (s : option ι → set α) : (⋃ o, s o) = s none ∪ ⋃ i, s (some i) :=
+supr_option s
+
+lemma Inter_option {ι} (s : option ι → set α) : (⋂ o, s o) = s none ∩ ⋂ i, s (some i) :=
+infi_option s
+
+/-! ### Bounded unions and intersections -/
 
 theorem mem_bUnion_iff {s : set α} {t : α → set β} {y : β} :
   y ∈ (⋃ x ∈ s, t x) ↔ ∃ x ∈ s, y ∈ t x := by simp
@@ -1156,6 +1160,14 @@ disjoint_sup_left
   disjoint s (t ∪ u) ↔ disjoint s t ∧ disjoint s u :=
 disjoint_sup_right
 
+@[simp] theorem disjoint_Union_left {ι : Sort*} {s : ι → set α} :
+  disjoint (⋃ i, s i) t ↔ ∀ i, disjoint (s i) t :=
+supr_disjoint_iff
+
+@[simp] theorem disjoint_Union_right {ι : Sort*} {s : ι → set α} :
+  disjoint t (⋃ i, s i) ↔ ∀ i, disjoint t (s i) :=
+disjoint_supr_iff
+
 theorem disjoint_diff {a b : set α} : disjoint a (b \ a) :=
 disjoint_iff.2 (inter_diff_self _ _)
 

src/order/complete_boolean_algebra.lean

@@ -23,17 +23,34 @@ class complete_distrib_lattice α extends complete_lattice α :=
 section complete_distrib_lattice
 variables [complete_distrib_lattice α] {a b : α} {s t : set α}
 
+instance : complete_distrib_lattice (order_dual α) :=
+{ infi_sup_le_sup_Inf := complete_distrib_lattice.inf_Sup_le_supr_inf,
+  inf_Sup_le_supr_inf := complete_distrib_lattice.infi_sup_le_sup_Inf,
+  .. order_dual.complete_lattice α }
+
 theorem sup_Inf_eq : a ⊔ Inf s = (⨅ b ∈ s, a ⊔ b) :=
 sup_Inf_le_infi_sup.antisymm (complete_distrib_lattice.infi_sup_le_sup_Inf _ _)
 
 theorem Inf_sup_eq : Inf s ⊔ b = (⨅ a ∈ s, a ⊔ b) :=
-by simpa [sup_comm] using @sup_Inf_eq α _ b s
+by simpa only [sup_comm] using @sup_Inf_eq α _ b s
 
 theorem inf_Sup_eq : a ⊓ Sup s = (⨆ b ∈ s, a ⊓ b) :=
 (complete_distrib_lattice.inf_Sup_le_supr_inf _ _).antisymm supr_inf_le_inf_Sup
 
 theorem Sup_inf_eq : Sup s ⊓ b = (⨆ a ∈ s, a ⊓ b) :=
-by simpa [inf_comm] using @inf_Sup_eq α _ b s
+by simpa only [inf_comm] using @inf_Sup_eq α _ b s
+
+theorem supr_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a :=
+by rw [supr, Sup_inf_eq, supr_range]
+
+theorem inf_supr_eq (a : α) (f : ι → α) : a ⊓ (⨆ i, f i) = ⨆ i, a ⊓ f i :=
+by simpa only [inf_comm] using supr_inf_eq f a
+
+theorem infi_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a :=
+@supr_inf_eq (order_dual α) _ _ _ _
+
+theorem sup_infi_eq (a : α) (f : ι → α) : a ⊔ (⨅ i, f i) = ⨅ i, a ⊔ f i :=
+@inf_supr_eq (order_dual α) _ _ _ _
 
 theorem Inf_sup_Inf : Inf s ⊔ Inf t = (⨅p ∈ set.prod s t, (p : α × α).1 ⊔ p.2) :=
 begin
@@ -58,26 +75,13 @@ begin
 end
 
 theorem Sup_inf_Sup : Sup s ⊓ Sup t = (⨆p ∈ set.prod s t, (p : α × α).1 ⊓ p.2) :=
-begin
-  apply le_antisymm,
-  { have : ∀ a ∈ s, a ⊓ Sup t ≤ (⨆p ∈ set.prod s t, (p : α × α).1 ⊓ p.2),
-    { assume a ha,
-      have : (⨆p ∈ prod.mk a '' t, (p : α × α).1 ⊓ p.2)
-             ≤ (⨆p ∈ set.prod s t, ((p : α × α).1 : α) ⊓ p.2),
-      { apply supr_le_supr_of_subset,
-        rintros ⟨x, y⟩,
-        simp only [and_imp, set.mem_image, prod.mk.inj_iff, set.prod_mk_mem_set_prod_eq,
-                   exists_imp_distrib],
-        assume x' x't ax x'y,
-        rw [← x'y, ← ax],
-        simp [ha, x't] },
-      rw [supr_image] at this,
-      simp only at this,
-      rwa ← inf_Sup_eq at this },
-    calc Sup s ⊓ Sup t = (⨆a∈s, a ⊓ Sup t) : Sup_inf_eq
-      ... ≤ (⨆p ∈ set.prod s t, (p : α × α).1 ⊓ p.2) : by simp; exact this },
-  { finish }
-end
+@Inf_sup_Inf (order_dual α) _ _ _
+
+lemma supr_disjoint_iff {f : ι → α} : disjoint (⨆ i, f i) a ↔ ∀ i, disjoint (f i) a :=
+by simp only [disjoint_iff, supr_inf_eq, supr_eq_bot]
+
+lemma disjoint_supr_iff {f : ι → α} : disjoint a (⨆ i, f i) ↔ ∀ i, disjoint a (f i) :=
+by simpa only [disjoint.comm] using @supr_disjoint_iff _ _ _ a f
 
 end complete_distrib_lattice
 

src/order/complete_lattice.lean

@@ -899,6 +899,14 @@ theorem supr_sum {γ : Type*} {f : β ⊕ γ → α} :
   (⨆ x, f x) = (⨆ i, f (sum.inl i)) ⊔ (⨆ j, f (sum.inr j)) :=
 @infi_sum (order_dual α) _ _ _ _
 
+theorem supr_option (f : option β → α) :
+  (⨆ o, f o) = f none ⊔ ⨆ b, f (option.some b) :=
+eq_of_forall_ge_iff $ λ c, by simp only [supr_le_iff, sup_le_iff, option.forall]
+
+theorem infi_option (f : option β → α) :
+  (⨅ o, f o) = f none ⊓ ⨅ b, f (option.some b) :=
+@supr_option (order_dual α) _ _ _
+
 /-!
 ### `supr` and `infi` under `ℕ`
 -/