From dcedc047cf9626a8f635281ffbb28ffe66fa7b7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Tue, 28 Jun 2022 03:59:01 +0000
Subject: [PATCH] feat(order/symm_diff): Triangle inequality for the symmetric
 difference (#14847)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Prove that `a ∆ c ≤ a ∆ b ⊔ b ∆ c`.
---
 src/order/boolean_algebra.lean |  6 ++++++
 src/order/symm_diff.lean       | 18 +++++++++++++++++-
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/order/boolean_algebra.lean b/src/order/boolean_algebra.lean
index 0c88c393a3864..ddbab6261809d 100644
--- a/src/order/boolean_algebra.lean
+++ b/src/order/boolean_algebra.lean
@@ -355,6 +355,12 @@ lemma sdiff_le_iff : y \ x ≤ z ↔ y ≤ x ⊔ z :=
 
 lemma sdiff_sdiff_le : x \ (x \ y) ≤ y := sdiff_le_iff.2 le_sdiff_sup
 
+lemma sdiff_triangle (x y z : α) : x \ z ≤ x \ y ⊔ y \ z :=
+begin
+  rw [sdiff_le_iff, sup_left_comm, ←sdiff_le_iff],
+  exact sdiff_sdiff_le.trans (sdiff_le_iff.1 le_rfl),
+end
+
 @[simp] lemma le_sdiff_iff : x ≤ y \ x ↔ x = ⊥ :=
 ⟨λ h, disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), λ h, h.le.trans bot_le⟩
 
diff --git a/src/order/symm_diff.lean b/src/order/symm_diff.lean
index 66b7d98df283d..d9ca1c0007027 100644
--- a/src/order/symm_diff.lean
+++ b/src/order/symm_diff.lean
@@ -21,7 +21,6 @@ The symmetric difference is the addition operator in the Boolean ring structure
 ## Main declarations
 
 * `symm_diff`: the symmetric difference operator, defined as `(A \ B) ⊔ (B \ A)`
-* `equiv.symm_diff`: Symmetric difference by `a` as an `equiv`.
 
 In generalized Boolean algebras, the symmetric difference operator is:
 
@@ -136,6 +135,16 @@ begin
   { exact h.symm_diff_eq_sup, },
 end
 
+@[simp] lemma le_symm_diff_iff_left : a ≤ a ∆ b ↔ disjoint a b :=
+begin
+  refine ⟨λ h, _, λ h, h.symm_diff_eq_sup.symm ▸ le_sup_left⟩,
+  rw symm_diff_eq_sup_sdiff_inf at h,
+  exact (le_sdiff_iff.1 $ inf_le_of_left_le h).le,
+end
+
+@[simp] lemma le_symm_diff_iff_right : b ≤ a ∆ b ↔ disjoint a b :=
+by rw [symm_diff_comm, le_symm_diff_iff_left, disjoint.comm]
+
 lemma symm_diff_symm_diff_left :
   a ∆ b ∆ c = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔ (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c) :=
 calc a ∆ b ∆ c = ((a ∆ b) \ c) ⊔ (c \ (a ∆ b))   : symm_diff_def _ _
@@ -160,6 +169,13 @@ 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]