[Merged by Bors] - feat(data/{multiset,finset}/sum): Disjoint sum of multisets/finsets

src/data/finset/sum.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.finset.card
+import data.multiset.sum
+/-!
+# Disjoint sum of finsets
+
+This file defines the disjoint sum of two finsets as `finset (α ⊕ β)`. Beware not to confuse with
+the `finset.sum` operation which computes the additive sum.
+
+## Main declarations
+
+* `finset.disj_sum`: `s.disj_sum t` is the disjoint sum of `s` and `t`.
+-/
+
+open function multiset sum
+
+namespace finset
+variables {α β : Type*} (s : finset α) (t : finset β)
+
+/-- Disjoint sum of finsets. -/
+def disj_sum : finset (α ⊕ β) := ⟨s.1.disj_sum t.1, s.2.disj_sum t.2⟩
+
+@[simp] lemma val_disj_sum : (s.disj_sum t).1 = s.1.disj_sum t.1 := rfl
+
+@[simp] lemma empty_disj_sum : (∅ : finset α).disj_sum t = t.map embedding.inr :=
+val_inj.1 $ multiset.zero_disj_sum _
+
+@[simp] lemma disj_sum_empty : s.disj_sum (∅ : finset β) = s.map embedding.inl :=
+val_inj.1 $ multiset.disj_sum_zero _
+
+@[simp] lemma card_disj_sum : (s.disj_sum t).card = s.card + t.card := multiset.card_disj_sum _ _
+
+variables {s t} {s₁ s₂ : finset α} {t₁ t₂ : finset β} {a : α} {b : β} {x : α ⊕ β}
+
+lemma mem_disj_sum : x ∈ s.disj_sum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x :=
+multiset.mem_disj_sum
+
+@[simp] lemma inl_mem_disj_sum : inl a ∈ s.disj_sum t ↔ a ∈ s := inl_mem_disj_sum
+@[simp] lemma inr_mem_disj_sum : inr b ∈ s.disj_sum t ↔ b ∈ t := inr_mem_disj_sum
+
+lemma disj_sum_mono (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : s₁.disj_sum t₁ ⊆ s₂.disj_sum t₂ :=
+val_le_iff.1 $ disj_sum_mono (val_le_iff.2 hs) (val_le_iff.2 ht)
+
+lemma disj_sum_mono_left (t : finset β) : monotone (λ s, s.disj_sum t) :=
+λ _ _ hs, disj_sum_mono hs subset.rfl
+
+lemma disj_sum_mono_right (s : finset α) : monotone (s.disj_sum : finset β → finset (α ⊕ β)) :=
+λ t₁ t₂, disj_sum_mono subset.rfl
+
+lemma disj_sum_ssubset_disj_sum_of_ssubset_of_subset (hs : s₁ ⊂ s₂) (ht : t₁ ⊆ t₂) :
+  s₁.disj_sum t₁ ⊂ s₂.disj_sum t₂ :=
+val_lt_iff.1 $ disj_sum_lt_disj_sum_of_lt_of_le (val_lt_iff.2 hs) (val_le_iff.2 ht)
+
+lemma disj_sum_ssubset_disj_sum_of_subset_of_ssubset (hs : s₁ ⊆ s₂) (ht : t₁ ⊂ t₂) :
+  s₁.disj_sum t₁ ⊂ s₂.disj_sum t₂ :=
+val_lt_iff.1 $ disj_sum_lt_disj_sum_of_le_of_lt (val_le_iff.2 hs) (val_lt_iff.2 ht)
+
+end finset

src/data/multiset/basic.lean

@@ -851,6 +851,16 @@ eq_of_mem_repeat $ by rwa map_const at h
 @[simp] theorem map_le_map {f : α → β} {s t : multiset α} (h : s ≤ t) : map f s ≤ map f t :=
 le_induction_on h $ λ l₁ l₂ h, (h.map f).subperm
 
+@[simp] lemma map_lt_map {f : α → β} {s t : multiset α} (h : s < t) : s.map f < t.map f :=
+begin
+  refine (map_le_map h.le).lt_of_not_le (λ H, h.ne $ eq_of_le_of_card_le h.le _),
+  rw [←s.card_map f, ←t.card_map f],
+  exact card_le_of_le H,
+end
+
+lemma map_mono (f : α → β) : monotone (map f) := λ _ _, map_le_map
+lemma map_strict_mono (f : α → β) : strict_mono (map f) := λ _ _, map_lt_map
+
 @[simp] theorem map_subset_map {f : α → β} {s t : multiset α} (H : s ⊆ t) : map f s ⊆ map f t :=
 λ b m, let ⟨a, h, e⟩ := mem_map.1 m in mem_map.2 ⟨a, H h, e⟩
 

src/data/multiset/sum.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.multiset.nodup
+
+/-!
+# Disjoint sum of multisets
+
+This file defines the disjoint sum of two multisets as `multiset (α ⊕ β)`. Beware not to confuse
+with the `multiset.sum` operation which computes the additive sum.
+
+## Main declarations
+
+* `multiset.disj_sum`: `s.disj_sum t` is the disjoint sum of `s` and `t`.
+-/
+
+open sum
+
+namespace multiset
+variables {α β : Type*} (s : multiset α) (t : multiset β)
+
+/-- Disjoint sum of multisets. -/
+def disj_sum : multiset (α ⊕ β) := s.map inl + t.map inr
+
+@[simp] lemma zero_disj_sum : (0 : multiset α).disj_sum t = t.map inr := zero_add _
+@[simp] lemma disj_sum_zero : s.disj_sum (0 : multiset β) = s.map inl := add_zero _
+
+@[simp] lemma card_disj_sum : (s.disj_sum t).card = s.card + t.card :=
+by rw [disj_sum, card_add, card_map, card_map]
+
+variables {s t} {s₁ s₂ : multiset α} {t₁ t₂ : multiset β} {a : α} {b : β} {x : α ⊕ β}
+
+lemma mem_disj_sum : x ∈ s.disj_sum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x :=
+by simp_rw [disj_sum, mem_add, mem_map]
+
+@[simp] lemma inl_mem_disj_sum : inl a ∈ s.disj_sum t ↔ a ∈ s :=
+begin
+  rw [mem_disj_sum, or_iff_left],
+  simp only [exists_eq_right],
+  rintro ⟨b, _, hb⟩,
+  exact inr_ne_inl hb,
+end
+
+@[simp] lemma inr_mem_disj_sum : inr b ∈ s.disj_sum t ↔ b ∈ t :=
+begin
+  rw [mem_disj_sum, or_iff_right],
+  simp only [exists_eq_right],
+  rintro ⟨a, _, ha⟩,
+  exact inl_ne_inr ha,
+end
+
+lemma disj_sum_mono (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) : s₁.disj_sum t₁ ≤ s₂.disj_sum t₂ :=
+add_le_add (map_le_map hs) (map_le_map ht)
+
+lemma disj_sum_mono_left (t : multiset β) : monotone (λ s, s.disj_sum t) :=
+λ _ _ hs,
+add_le_add_right (map_le_map hs) _
+
+lemma disj_sum_mono_right (s : multiset α) :
+  monotone (s.disj_sum : multiset β → multiset (α ⊕ β)) :=
+λ t₁ t₂ ht, add_le_add_left (map_le_map ht) _
+
+lemma disj_sum_lt_disj_sum_of_lt_of_le (hs : s₁ < s₂) (ht : t₁ ≤ t₂) :
+  s₁.disj_sum t₁ < s₂.disj_sum t₂ :=
+add_lt_add_of_lt_of_le (map_lt_map hs) (map_le_map ht)
+
+lemma disj_sum_lt_disj_sum_of_le_of_lt (hs : s₁ ≤ s₂) (ht : t₁ < t₂) :
+  s₁.disj_sum t₁ < s₂.disj_sum t₂ :=
+add_lt_add_of_le_of_lt (map_le_map hs) (map_lt_map ht)
+
+protected lemma nodup.disj_sum (hs : s.nodup) (ht : t.nodup) : (s.disj_sum t).nodup :=
+begin
+  refine (multiset.nodup_add_of_nodup (multiset.nodup_map inl_injective hs) $
+    multiset.nodup_map inr_injective ht).2 (λ x hs ht, _),
+  rw multiset.mem_map at hs ht,
+  obtain ⟨a, _, rfl⟩ := hs,
+  obtain ⟨b, _, h⟩ := ht,
+  exact inr_ne_inl h,
+end
+
+end multiset

src/logic/basic.lean

@@ -507,6 +507,9 @@ theorem not_imp_not : (¬ a → ¬ b) ↔ (b → a) := decidable.not_imp_not
 @[simp] theorem or_iff_right_iff_imp : (a ∨ b ↔ b) ↔ (a → b) :=
 by rw [or_comm, or_iff_left_iff_imp]
 
+lemma or_iff_left (hb : ¬ b) : a ∨ b ↔ a := ⟨λ h, h.resolve_right hb, or.inl⟩
+lemma or_iff_right (ha : ¬ a) : a ∨ b ↔ b := ⟨λ h, h.resolve_left ha, or.inr⟩
+
 /-! ### Declarations about distributivity -/
 
 /-- `∧` distributes over `∨` (on the left). -/