diff --git a/src/data/dfinsupp/interval.lean b/src/data/dfinsupp/interval.lean index e231a1c5849d6..2516db9bbc19a 100644 --- a/src/data/dfinsupp/interval.lean +++ b/src/data/dfinsupp/interval.lean @@ -92,10 +92,10 @@ def range_Icc (f g : Π₀ i, α i) : Π₀ i, finset (α i) := { to_fun := λ i, Icc (f i) (g i), support' := f.support'.bind $ λ fs, g.support'.map $ λ gs, ⟨fs + gs, λ i, or_iff_not_imp_left.2 $ λ h, begin - have hf : f i = 0 := - (fs.prop i).resolve_left (multiset.not_mem_mono (multiset.le_add_right _ _).subset h), - have hg : g i = 0 := - (gs.prop i).resolve_left (multiset.not_mem_mono (multiset.le_add_left _ _).subset h), + have hf : f i = 0 := (fs.prop i).resolve_left + (multiset.not_mem_mono (multiset.le.subset $ multiset.le_add_right _ _) h), + have hg : g i = 0 := (gs.prop i).resolve_left + (multiset.not_mem_mono (multiset.le.subset $ multiset.le_add_left _ _) h), rw [hf, hg], exact Icc_self _, end⟩ } diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index a12082e020a13..cc369ee8984ad 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -1339,6 +1339,13 @@ sup_eq_sdiff_sup_sdiff_sup_inf lemma erase_eq_empty_iff (s : finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a} := by rw [←sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff] +/-! ### Symmetric difference -/ + +lemma mem_symm_diff : a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s := +by simp_rw [symm_diff, sup_eq_union, mem_union, mem_sdiff] + +@[simp, norm_cast] lemma coe_symm_diff : (↑(s ∆ t) : set α) = s ∆ t := set.ext $ λ _, mem_symm_diff + end decidable_eq /-! ### attach -/ diff --git a/src/data/set/basic.lean b/src/data/set/basic.lean index e357532fd41ec..4e3af611b712c 100644 --- a/src/data/set/basic.lean +++ b/src/data/set/basic.lean @@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura -/ -import order.boolean_algebra +import order.symm_diff /-! # Basic properties of sets @@ -77,7 +77,7 @@ universes u v w x namespace set -variable {α : Type*} +variables {α : Type*} {s t : set α} instance : has_le (set α) := ⟨λ s t, ∀ ⦃x⦄, x ∈ s → x ∈ t⟩ instance : has_subset (set α) := ⟨(≤)⟩ @@ -104,6 +104,12 @@ instance : has_inter (set α) := ⟨(⊓)⟩ @[simp] lemma le_eq_subset : ((≤) : set α → set α → Prop) = (⊆) := rfl @[simp] lemma lt_eq_ssubset : ((<) : set α → set α → Prop) = (⊂) := rfl +lemma le_iff_subset : s ≤ t ↔ s ⊆ t := iff.rfl +lemma lt_iff_ssubset : s ≤ t ↔ s ⊆ t := iff.rfl + +alias le_iff_subset ↔ _root_.has_le.le.subset _root_.has_subset.subset.le +alias lt_iff_ssubset ↔ _root_.has_lt.lt.ssubset _root_.has_ssubset.ssubset.lt + /-- Coercion from a set to the corresponding subtype. -/ instance {α : Type u} : has_coe_to_sort (set α) (Type u) := ⟨λ s, {x // x ∈ s}⟩ @@ -1178,6 +1184,18 @@ lemma union_eq_diff_union_diff_union_inter (s t : set α) : s ∪ t = (s \ t) ∪ (t \ s) ∪ (s ∩ t) := sup_eq_sdiff_sup_sdiff_sup_inf +/-! ### Symmetric difference -/ + +lemma mem_symm_diff : a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s := iff.rfl + +lemma symm_diff_subset_union : s ∆ t ⊆ s ∪ t := @symm_diff_le_sup (set α) _ _ _ + +lemma inter_symm_diff_distrib_left (s t u : set α) : s ∩ t ∆ u = (s ∩ t) ∆ (s ∩ u) := +inf_symm_diff_distrib_left _ _ _ + +lemma inter_symm_diff_distrib_right (s t u : set α) : s ∆ t ∩ u = (s ∩ u) ∆ (t ∩ u) := +inf_symm_diff_distrib_right _ _ _ + /-! ### Powerset -/ /-- `𝒫 s = set.powerset s` is the set of all subsets of `s`. -/ diff --git a/src/measure_theory/decomposition/jordan.lean b/src/measure_theory/decomposition/jordan.lean index e1cad89cc5703..e8d762e73b939 100644 --- a/src/measure_theory/decomposition/jordan.lean +++ b/src/measure_theory/decomposition/jordan.lean @@ -169,7 +169,7 @@ end jordan_decomposition namespace signed_measure -open measure vector_measure jordan_decomposition classical +open classical jordan_decomposition measure set vector_measure variables {s : signed_measure α} {μ ν : measure α} [is_finite_measure μ] [is_finite_measure ν] @@ -293,12 +293,9 @@ lemma of_inter_eq_of_symm_diff_eq_zero_positive begin have hwuv : s ((w ∩ u) ∆ (w ∩ v)) = 0, { refine subset_positive_null_set (hu.union hv) ((hw.inter hu).symm_diff (hw.inter hv)) - (hu.symm_diff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs _ _, - { exact symm_diff_le_sup u v }, - { rintro x (⟨⟨hxw, hxu⟩, hx⟩ | ⟨⟨hxw, hxv⟩, hx⟩); - rw [set.mem_inter_eq, not_and] at hx, - { exact or.inl ⟨hxu, hx hxw⟩ }, - { exact or.inr ⟨hxv, hx hxw⟩ } } }, + (hu.symm_diff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs symm_diff_subset_union _, + rw ←inter_symm_diff_distrib_left, + exact inter_subset_right _ _ }, obtain ⟨huv, hvu⟩ := of_diff_eq_zero_of_symm_diff_eq_zero_positive (hw.inter hu) (hw.inter hv) (restrict_le_restrict_subset _ _ hu hsu (w.inter_subset_right u)) diff --git a/src/order/symm_diff.lean b/src/order/symm_diff.lean index d9ca1c0007027..dd9529d82c243 100644 --- a/src/order/symm_diff.lean +++ b/src/order/symm_diff.lean @@ -44,23 +44,23 @@ boolean ring, generalized boolean algebra, boolean algebra, symmetric difference open function +variables {α : Type*} + /-- The symmetric difference operator on a type with `⊔` and `\` is `(A \ B) ⊔ (B \ A)`. -/ -def symm_diff {α : Type*} [has_sup α] [has_sdiff α] (A B : α) : α := (A \ B) ⊔ (B \ A) +def symm_diff [has_sup α] [has_sdiff α] (a b : α) : α := a \ b ⊔ b \ a /- This notation might conflict with the Laplacian once we have it. Feel free to put it in locale `order` or `symm_diff` if that happens. -/ infix ` ∆ `:100 := symm_diff -lemma symm_diff_def {α : Type*} [has_sup α] [has_sdiff α] (A B : α) : - A ∆ B = (A \ B) ⊔ (B \ A) := -rfl +lemma symm_diff_def [has_sup α] [has_sdiff α] (a b : α) : a ∆ b = (a \ b) ⊔ (b \ a) := rfl lemma symm_diff_eq_xor (p q : Prop) : p ∆ q = xor p q := rfl @[simp] lemma bool.symm_diff_eq_bxor : ∀ p q : bool, p ∆ q = bxor p q := dec_trivial -section generalized_boolean_algebra -variables {α : Type*} [generalized_boolean_algebra α] (a b c d : α) +section generalized_coheyting_algebra +variables [generalized_coheyting_algebra α] (a b c d : α) lemma symm_diff_comm : a ∆ b = b ∆ a := by simp only [(∆), sup_comm] @@ -70,8 +70,86 @@ instance symm_diff_is_comm : is_commutative α (∆) := ⟨symm_diff_comm⟩ @[simp] lemma symm_diff_bot : a ∆ ⊥ = a := by rw [(∆), sdiff_bot, bot_sdiff, sup_bot_eq] @[simp] lemma bot_symm_diff : ⊥ ∆ a = a := by rw [symm_diff_comm, symm_diff_bot] -lemma symm_diff_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b) := -by simp [sup_sdiff, sdiff_inf, sup_comm, (∆)] +lemma symm_diff_of_le {a b : α} (h : a ≤ b) : a ∆ b = b \ a := +by rw [symm_diff, sdiff_eq_bot_iff.2 h, bot_sup_eq] + +lemma symm_diff_of_ge {a b : α} (h : b ≤ a) : a ∆ b = a \ b := +by rw [symm_diff, sdiff_eq_bot_iff.2 h, sup_bot_eq] + +lemma symm_diff_le {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ∆ b ≤ c := +sup_le (sdiff_le_iff.2 ha) $ sdiff_le_iff.2 hb + +lemma symm_diff_le_iff {a b c : α} : a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c := +by simp_rw [symm_diff, sup_le_iff, sdiff_le_iff] + +@[simp] lemma symm_diff_le_sup {a b : α} : a ∆ b ≤ a ⊔ b := sup_le_sup sdiff_le sdiff_le + +lemma symm_diff_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b) := by simp [sup_sdiff, symm_diff] + +lemma disjoint.symm_diff_eq_sup {a b : α} (h : disjoint a b) : a ∆ b = a ⊔ b := +by rw [(∆), h.sdiff_eq_left, h.sdiff_eq_right] + +lemma symm_diff_sdiff : (a ∆ b) \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) := +by rw [symm_diff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left] + +@[simp] lemma symm_diff_sdiff_inf : a ∆ b \ (a ⊓ b) = a ∆ b := +by { rw symm_diff_sdiff, simp [symm_diff] } + +@[simp] lemma symm_diff_sdiff_eq_sup : a ∆ (b \ a) = a ⊔ b := +begin + rw [symm_diff, sdiff_idem], + exact le_antisymm (sup_le_sup sdiff_le sdiff_le) + (sup_le le_sdiff_sup $ le_sdiff_sup.trans $ sup_le le_sup_right le_sdiff_sup), +end + +@[simp] lemma sdiff_symm_diff_eq_sup : (a \ b) ∆ b = a ⊔ b := +by rw [symm_diff_comm, symm_diff_sdiff_eq_sup, sup_comm] + +@[simp] lemma symm_diff_sup_inf : a ∆ b ⊔ a ⊓ b = a ⊔ b := +begin + refine le_antisymm (sup_le symm_diff_le_sup inf_le_sup) _, + rw [sup_inf_left, symm_diff], + refine sup_le (le_inf le_sup_right _) (le_inf _ le_sup_right), + { rw sup_right_comm, + exact le_sup_of_le_left le_sdiff_sup }, + { rw sup_assoc, + exact le_sup_of_le_right le_sdiff_sup } +end + +@[simp] lemma inf_sup_symm_diff : a ⊓ b ⊔ a ∆ b = a ⊔ b := by rw [sup_comm, symm_diff_sup_inf] + +@[simp] lemma symm_diff_symm_diff_inf : a ∆ b ∆ (a ⊓ b) = a ⊔ b := +by rw [←symm_diff_sdiff_inf a, sdiff_symm_diff_eq_sup, symm_diff_sup_inf] + +@[simp] lemma inf_symm_diff_symm_diff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b := +by rw [symm_diff_comm, symm_diff_symm_diff_inf] + +lemma symm_diff_triangle : a ∆ c ≤ a ∆ b ⊔ b ∆ c := +begin + refine (sup_le_sup (sdiff_triangle a b c) $ sdiff_triangle _ b _).trans_eq _, + rw [@sup_comm _ _ (c \ b), sup_sup_sup_comm, symm_diff, symm_diff], +end + +end generalized_coheyting_algebra + +section coheyting_algebra +variables [coheyting_algebra α] (a : α) + +@[simp] lemma symm_diff_top' : a ∆ ⊤ = ￢a := by simp [symm_diff] +@[simp] lemma top_symm_diff' : ⊤ ∆ a = ￢a := by simp [symm_diff] + +@[simp] lemma hnot_symm_diff_self : (￢a) ∆ a = ⊤ := +by { rw [eq_top_iff, symm_diff, hnot_sdiff, sup_sdiff_self], exact codisjoint_hnot_left } + +@[simp] lemma symm_diff_hnot_self : a ∆ ￢a = ⊤ := by rw [symm_diff_comm, hnot_symm_diff_self] + +lemma is_compl.symm_diff_eq_top {a b : α} (h : is_compl a b) : a ∆ b = ⊤ := +by rw [h.eq_hnot, hnot_symm_diff_self] + +end coheyting_algebra + +section generalized_boolean_algebra +variables [generalized_boolean_algebra α] (a b c d : α) @[simp] lemma sup_sdiff_symm_diff : (a ⊔ b) \ (a ∆ b) = a ⊓ b := sdiff_eq_symm inf_le_sup (by rw symm_diff_eq_sup_sdiff_inf) @@ -82,8 +160,6 @@ begin exact disjoint_sdiff_self_left, end -lemma symm_diff_le_sup : a ∆ b ≤ a ⊔ b := by { rw symm_diff_eq_sup_sdiff_inf, exact sdiff_le } - lemma inf_symm_diff_distrib_left : a ⊓ (b ∆ c) = (a ⊓ b) ∆ (a ⊓ c) := by rw [symm_diff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left, symm_diff_eq_sup_sdiff_inf] @@ -97,9 +173,6 @@ by simp only [(∆), sdiff_sdiff_sup_sdiff'] lemma sdiff_symm_diff' : c \ (a ∆ b) = (c ⊓ a ⊓ b) ⊔ (c \ (a ⊔ b)) := by rw [sdiff_symm_diff, sdiff_sup, sup_comm] -lemma symm_diff_sdiff : (a ∆ b) \ c = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) := -by rw [symm_diff_def, sup_sdiff, sdiff_sdiff_left, sdiff_sdiff_left] - @[simp] lemma symm_diff_sdiff_left : (a ∆ b) \ a = b \ a := by rw [symm_diff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq] @@ -108,31 +181,11 @@ by rw [symm_diff_comm, symm_diff_sdiff_left] @[simp] lemma sdiff_symm_diff_self : a \ (a ∆ b) = a ⊓ b := by simp [sdiff_symm_diff] -lemma symm_diff_eq_iff_sdiff_eq {a b c : α} (ha : a ≤ c) : - a ∆ b = c ↔ c \ a = b := -begin - split; intro h, - { have hba : disjoint (a ⊓ b) c := begin - rw [←h, disjoint.comm], - exact disjoint_symm_diff_inf _ _, - end, - have hca : _ := congr_arg (\ a) h, - rw [symm_diff_sdiff_left] at hca, - rw [←hca, sdiff_eq_self_iff_disjoint], - exact hba.of_disjoint_inf_of_le ha }, - { have hd : disjoint a b := by { rw ←h, exact disjoint_sdiff_self_right }, - rw [symm_diff_def, hd.sdiff_eq_left, hd.sdiff_eq_right, ←h, sup_sdiff_cancel_right ha] } -end - -lemma disjoint.symm_diff_eq_sup {a b : α} (h : disjoint a b) : a ∆ b = a ⊔ b := -by rw [(∆), h.sdiff_eq_left, h.sdiff_eq_right] - lemma symm_diff_eq_sup : a ∆ b = a ⊔ b ↔ disjoint a b := begin - split; intro h, - { rw [symm_diff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h, - exact h.of_disjoint_inf_of_le le_sup_left, }, - { exact h.symm_diff_eq_sup, }, + refine ⟨λ h, _, disjoint.symm_diff_eq_sup⟩, + rw [symm_diff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h, + exact h.of_disjoint_inf_of_le le_sup_left, end @[simp] lemma le_symm_diff_iff_left : a ≤ a ∆ b ↔ disjoint a b := @@ -163,19 +216,6 @@ calc a ∆ (b ∆ c) = (a \ (b ∆ c)) ⊔ ((b ∆ c) \ a) : symm_diff_def _ _ ... = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔ (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c) : by ac_refl -@[simp] lemma symm_diff_symm_diff_inf : a ∆ b ∆ (a ⊓ b) = a ⊔ b := -by rw [symm_diff_eq_iff_sdiff_eq (symm_diff_le_sup _ _), sup_sdiff_symm_diff] - -@[simp] lemma inf_symm_diff_symm_diff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b := -by rw [symm_diff_comm, symm_diff_symm_diff_inf] - -lemma symm_diff_triangle : a ∆ c ≤ a ∆ b ⊔ b ∆ c := -begin - refine (sup_le_sup (sdiff_triangle a b c) $ sdiff_triangle _ b _).trans_eq _, - rw [@sup_comm _ _ (c \ b), sup_sup_sup_comm], - refl, -end - lemma symm_diff_assoc : a ∆ b ∆ c = a ∆ (b ∆ c) := by rw [symm_diff_symm_diff_left, symm_diff_symm_diff_right] @@ -228,15 +268,21 @@ protected lemma disjoint.symm_diff_right (ha : disjoint a b) (hb : disjoint a c) disjoint a (b ∆ c) := (ha.symm.symm_diff_left hb.symm).symm +lemma symm_diff_eq_iff_sdiff_eq (ha : a ≤ c) : a ∆ b = c ↔ c \ a = b := +begin + rw ←symm_diff_of_le ha, + exact ((symm_diff_right_involutive a).to_perm _).apply_eq_iff_eq_symm_apply.trans eq_comm, +end + end generalized_boolean_algebra section boolean_algebra -variables {α : Type*} [boolean_algebra α] (a b c : α) +variables [boolean_algebra α] (a b c : α) lemma symm_diff_eq : a ∆ b = (a ⊓ bᶜ) ⊔ (b ⊓ aᶜ) := by simp only [(∆), sdiff_eq] -@[simp] lemma symm_diff_top : a ∆ ⊤ = aᶜ := by simp [symm_diff_eq] -@[simp] lemma top_symm_diff : ⊤ ∆ a = aᶜ := by rw [symm_diff_comm, symm_diff_top] +lemma symm_diff_top : a ∆ ⊤ = aᶜ := symm_diff_top' _ +lemma top_symm_diff : ⊤ ∆ a = aᶜ := top_symm_diff' _ lemma compl_symm_diff : (a ∆ b)ᶜ = (a ⊓ b) ⊔ (aᶜ ⊓ bᶜ) := by simp only [←top_sdiff, sdiff_symm_diff, top_inf_eq] @@ -244,12 +290,8 @@ by simp only [←top_sdiff, sdiff_symm_diff, top_inf_eq] lemma symm_diff_eq_top_iff : a ∆ b = ⊤ ↔ is_compl a b := by rw [symm_diff_eq_iff_sdiff_eq le_top, top_sdiff, compl_eq_iff_is_compl] -lemma is_compl.symm_diff_eq_top (h : is_compl a b) : a ∆ b = ⊤ := (symm_diff_eq_top_iff a b).2 h - -@[simp] lemma compl_symm_diff_self : aᶜ ∆ a = ⊤ := -by simp only [symm_diff_eq, compl_compl, inf_idem, compl_sup_eq_top] - -@[simp] lemma symm_diff_compl_self : a ∆ aᶜ = ⊤ := by rw [symm_diff_comm, compl_symm_diff_self] +@[simp] lemma compl_symm_diff_self : aᶜ ∆ a = ⊤ := hnot_symm_diff_self _ +@[simp] lemma symm_diff_compl_self : a ∆ aᶜ = ⊤ := symm_diff_hnot_self _ lemma symm_diff_symm_diff_right' : a ∆ (b ∆ c) = (a ⊓ b ⊓ c) ⊔ (a ⊓ bᶜ ⊓ cᶜ) ⊔ (aᶜ ⊓ b ⊓ cᶜ) ⊔ (aᶜ ⊓ bᶜ ⊓ c) :=