chore(order/symm_diff): Change the symmetric difference notation (#13217

)

The notation for `symm_diff` was `Δ` (`\D`, `\GD`, `\Delta`). It now is `∆` (`\increment`).

src/combinatorics/colex.lean

@@ -71,7 +71,7 @@ lemma colex.eq_iff (A B : finset α) :
 
 /--
 `A` is less than `B` in the colex ordering if the largest thing that's not in both sets is in B.
-In other words, max (A Δ B) ∈ B (if the maximum exists).
+In other words, `max (A ∆ B) ∈ B` (if the maximum exists).
 -/
 instance [has_lt α] : has_lt (finset.colex α) :=
 ⟨λ (A B : finset α), ∃ (k : α), (∀ {x}, k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A ∧ k ∈ B⟩

src/data/mv_polynomial/basic.lean

@@ -543,7 +543,7 @@ begin
 end
 
 lemma support_symm_diff_support_subset_support_add [decidable_eq σ] (p q : mv_polynomial σ R) :
-  p.support Δ q.support ⊆ (p + q).support :=
+  p.support ∆ q.support ⊆ (p + q).support :=
 begin
   rw [symm_diff_def, finset.sup_eq_union],
   apply finset.union_subset,

src/measure_theory/decomposition/jordan.lean

@@ -259,7 +259,7 @@ end
 between the two sets. -/
 lemma of_diff_eq_zero_of_symm_diff_eq_zero_positive
   (hu : measurable_set u) (hv : measurable_set v)
-  (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u Δ v) = 0) :
+  (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) :
   s (u \ v) = 0 ∧ s (v \ u) = 0 :=
 begin
   rw restrict_le_restrict_iff at hsu hsv,
@@ -276,7 +276,7 @@ end
 between the two sets. -/
 lemma of_diff_eq_zero_of_symm_diff_eq_zero_negative
   (hu : measurable_set u) (hv : measurable_set v)
-  (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u Δ v) = 0) :
+  (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) :
   s (u \ v) = 0 ∧ s (v \ u) = 0 :=
 begin
   rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu,
@@ -288,10 +288,10 @@ end
 
 lemma of_inter_eq_of_symm_diff_eq_zero_positive
   (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w)
-  (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u Δ v) = 0) :
+  (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) :
   s (w ∩ u) = s (w ∩ v) :=
 begin
-  have hwuv : s ((w ∩ u) Δ (w ∩ v)) = 0,
+  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 },
@@ -308,7 +308,7 @@ end
 
 lemma of_inter_eq_of_symm_diff_eq_zero_negative
   (hu : measurable_set u) (hv : measurable_set v) (hw : measurable_set w)
-  (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u Δ v) = 0) :
+  (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) :
   s (w ∩ u) = s (w ∩ v) :=
 begin
   rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu,

src/measure_theory/decomposition/signed_hahn.lean

@@ -412,7 +412,7 @@ begin
   refine ⟨Aᶜ, hA₁.compl, _, (compl_compl A).symm ▸ hA₂⟩,
   rw restrict_le_restrict_iff _ _ hA₁.compl,
   intros C hC hC₁,
-  by_contra' hC₂, 
+  by_contra' hC₂,
   rcases exists_subset_restrict_nonpos hC₂ with ⟨D, hD₁, hD, hD₂, hD₃⟩,
   have : s (A ∪ D) < Inf s.measure_of_negatives,
   { rw [← hA₃, of_union (set.disjoint_of_subset_right (set.subset.trans hD hC₁)
@@ -435,7 +435,7 @@ let ⟨i, hi₁, hi₂, hi₃⟩ := exists_compl_positive_negative s in
 lemma of_symm_diff_compl_positive_negative {s : signed_measure α}
   {i j : set α} (hi : measurable_set i) (hj : measurable_set j)
   (hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0) (hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0) :
-  s (i Δ j) = 0 ∧ s (iᶜ Δ jᶜ) = 0 :=
+  s (i ∆ j) = 0 ∧ s (iᶜ ∆ jᶜ) = 0 :=
 begin
   rw [restrict_le_restrict_iff s 0, restrict_le_restrict_iff 0 s] at hi' hj',
   split,

src/measure_theory/measurable_space_def.lean

@@ -194,7 +194,7 @@ h₁.inter h₂.compl
 
 @[simp] lemma measurable_set.symm_diff {s₁ s₂ : set α}
   (h₁ : measurable_set s₁) (h₂ : measurable_set s₂) :
-  measurable_set (s₁ Δ s₂) :=
+  measurable_set (s₁ ∆ s₂) :=
 (h₁.diff h₂).union (h₂.diff h₁)
 
 @[simp] lemma measurable_set.ite {t s₁ s₂ : set α} (ht : measurable_set t) (h₁ : measurable_set s₁)

src/order/imp.lean

@@ -12,7 +12,7 @@ import tactic.monotonicity.basic
 In this file we define `lattice.imp` (notation: `a ⇒ₒ b`) and `lattice.biimp` (notation: `a ⇔ₒ b`)
 to be the implication and equivalence as operations on a boolean algebra. More precisely, we put
 `a ⇒ₒ b = aᶜ ⊔ b` and `a ⇔ₒ b = (a ⇒ₒ b) ⊓ (b ⇒ₒ a)`. Equivalently, `a ⇒ₒ b = (a \ b)ᶜ` and
-`a ⇔ₒ b = (a Δ b)ᶜ`. For propositions these operations are equal to the usual implication and `iff`.
+`a ⇔ₒ b = (a ∆ b)ᶜ`. For propositions these operations are equal to the usual implication and `iff`.
 -/
 
 variables {α β : Type*}
@@ -84,10 +84,10 @@ by simp [biimp, ← le_antisymm_iff]
 
 lemma biimp_symm : a ≤ (b ⇔ₒ c) ↔ a ≤ (c ⇔ₒ b) := by rw biimp_comm
 
-lemma compl_symm_diff (a b : α) : (a Δ b)ᶜ = a ⇔ₒ b :=
+lemma compl_symm_diff (a b : α) : (a ∆ b)ᶜ = a ⇔ₒ b :=
 by simp only [biimp, imp, symm_diff, sdiff_eq, compl_sup, compl_inf, compl_compl]
 
-lemma compl_biimp (a b : α) : (a ⇔ₒ b)ᶜ = a Δ b := by rw [← compl_symm_diff, compl_compl]
+lemma compl_biimp (a b : α) : (a ⇔ₒ b)ᶜ = a ∆ b := by rw [← compl_symm_diff, compl_compl]
 
 @[simp] lemma compl_biimp_compl : aᶜ ⇔ₒ bᶜ = a ⇔ₒ b := by simp [biimp, inf_comm]
 

src/order/symm_diff.lean

@@ -29,7 +29,7 @@ In generalized Boolean algebras, the symmetric difference operator is:
 
 ## Notations
 
-* `a Δ b`: `symm_diff a b`
+* `a ∆ b`: `symm_diff a b`
 
 ## References
 
@@ -45,65 +45,67 @@ boolean ring, generalized boolean algebra, boolean algebra, symmetric difference
 /-- 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)
 
-infix ` Δ `:100 := symm_diff
+/- 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) :=
+  A ∆ B = (A \ B) ⊔ (B \ A) :=
 rfl
 
-lemma symm_diff_eq_xor (p q : Prop) : p Δ q = xor p q := rfl
+lemma symm_diff_eq_xor (p q : Prop) : p ∆ q = xor p q := rfl
 
 section generalized_boolean_algebra
 variables {α : Type*} [generalized_boolean_algebra α] (a b c : α)
 
-lemma symm_diff_comm : a Δ b = b Δ a := by simp only [(Δ), sup_comm]
+lemma symm_diff_comm : a ∆ b = b ∆ a := by simp only [(∆), sup_comm]
 
-instance symm_diff_is_comm : is_commutative α (Δ) := ⟨symm_diff_comm⟩
+instance symm_diff_is_comm : is_commutative α (∆) := ⟨symm_diff_comm⟩
 
-@[simp] lemma symm_diff_self : a Δ a = ⊥ := by rw [(Δ), sup_idem, sdiff_self]
-@[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]
+@[simp] lemma symm_diff_self : a ∆ a = ⊥ := by rw [(∆), sup_idem, sdiff_self]
+@[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_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b) :=
+by simp [sup_sdiff, sdiff_inf, sup_comm, (∆)]
 
-@[simp] lemma sup_sdiff_symm_diff : (a ⊔ b) \ (a Δ b) = a ⊓ b :=
+@[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)
 
-lemma disjoint_symm_diff_inf : disjoint (a Δ b) (a ⊓ b) :=
+lemma disjoint_symm_diff_inf : disjoint (a ∆ b) (a ⊓ b) :=
 begin
   rw [symm_diff_eq_sup_sdiff_inf],
   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 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) :=
+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]
 
-lemma inf_symm_diff_distrib_right : (a Δ b) ⊓ c = (a ⊓ c) Δ (b ⊓ c) :=
+lemma inf_symm_diff_distrib_right : (a ∆ b) ⊓ c = (a ⊓ c) ∆ (b ⊓ c) :=
 by simp_rw [@inf_comm _ _ _ c, inf_symm_diff_distrib_left]
 
-lemma sdiff_symm_diff : c \ (a Δ b) = (c ⊓ a ⊓ b) ⊔ ((c \ a) ⊓ (c \ b)) :=
-by simp only [(Δ), sdiff_sdiff_sup_sdiff']
+lemma sdiff_symm_diff : c \ (a ∆ b) = (c ⊓ a ⊓ b) ⊔ ((c \ a) ⊓ (c \ b)) :=
+by simp only [(∆), sdiff_sdiff_sup_sdiff']
 
-lemma sdiff_symm_diff' : c \ (a Δ b) = (c ⊓ a ⊓ b) ⊔ (c \ (a ⊔ b)) :=
+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)) :=
+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 :=
+@[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]
 
-@[simp] lemma symm_diff_sdiff_right : (a Δ b) \ b = a \ b :=
+@[simp] lemma symm_diff_sdiff_right : (a ∆ b) \ b = a \ b :=
 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]
+@[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 :=
+  a ∆ b = c ↔ c \ a = b :=
 begin
   split; intro h,
   { have hba : disjoint (a ⊓ b) c := begin
@@ -118,10 +120,10 @@ begin
     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 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 :=
+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,
@@ -130,96 +132,96 @@ begin
 end
 
 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 _ _
+  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 _ _
            ... = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔
                    ((c \ (a ⊔ b)) ⊔ (c ⊓ a ⊓ b)) :
                                 by rw [sdiff_symm_diff', @sup_comm _ _ (c ⊓ a ⊓ b), symm_diff_sdiff]
            ... = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔
                    (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c)   : by ac_refl
 
 lemma symm_diff_symm_diff_right :
-  a Δ (b Δ c) = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔ (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c) :=
-calc a Δ (b Δ c) = (a \ (b Δ c)) ⊔ ((b Δ c) \ a) : symm_diff_def _ _
+  a ∆ (b ∆ c) = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔ (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c) :=
+calc a ∆ (b ∆ c) = (a \ (b ∆ c)) ⊔ ((b ∆ c) \ a) : symm_diff_def _ _
              ... = (a \ (b ⊔ c)) ⊔ (a ⊓ b ⊓ c) ⊔
                      (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))   :
                                 by rw [sdiff_symm_diff', @sup_comm _ _ (a ⊓ b ⊓ c), symm_diff_sdiff]
              ... = (a \ (b ⊔ c)) ⊔ (b \ (a ⊔ c)) ⊔
                      (c \ (a ⊔ b)) ⊔ (a ⊓ b ⊓ c)   : by ac_refl
 
-lemma symm_diff_assoc : a Δ b Δ c = a Δ (b Δ c) :=
+lemma symm_diff_assoc : a ∆ b ∆ c = a ∆ (b ∆ c) :=
 by rw [symm_diff_symm_diff_left, symm_diff_symm_diff_right]
 
-instance symm_diff_is_assoc : is_associative α (Δ) := ⟨symm_diff_assoc⟩
+instance symm_diff_is_assoc : is_associative α (∆) := ⟨symm_diff_assoc⟩
 
-@[simp] lemma symm_diff_symm_diff_self : a Δ (a Δ b) = b := by simp [←symm_diff_assoc]
+@[simp] lemma symm_diff_symm_diff_self : a ∆ (a ∆ b) = b := by simp [←symm_diff_assoc]
 
-@[simp] lemma symm_diff_symm_diff_self' : a Δ b Δ a = b :=
+@[simp] lemma symm_diff_symm_diff_self' : a ∆ b ∆ a = b :=
 by rw [symm_diff_comm, ←symm_diff_assoc, symm_diff_self, bot_symm_diff]
 
-@[simp] lemma symm_diff_right_inj : a Δ b = a Δ c ↔ b = c :=
+@[simp] lemma symm_diff_right_inj : a ∆ b = a ∆ c ↔ b = c :=
 begin
   split; intro h,
-  { have H1 := congr_arg ((Δ) a) h,
+  { have H1 := congr_arg ((∆) a) h,
     rwa [symm_diff_symm_diff_self, symm_diff_symm_diff_self] at H1, },
   { rw h, },
 end
 
-@[simp] lemma symm_diff_left_inj : a Δ b = c Δ b ↔ a = c :=
+@[simp] lemma symm_diff_left_inj : a ∆ b = c ∆ b ↔ a = c :=
 by rw [symm_diff_comm a b, symm_diff_comm c b, symm_diff_right_inj]
 
-@[simp] lemma symm_diff_eq_left : a Δ b = a ↔ b = ⊥ :=
-calc a Δ b = a ↔ a Δ b = a Δ ⊥ : by rw symm_diff_bot
+@[simp] lemma symm_diff_eq_left : a ∆ b = a ↔ b = ⊥ :=
+calc a ∆ b = a ↔ a ∆ b = a ∆ ⊥ : by rw symm_diff_bot
            ... ↔     b = ⊥     : by rw symm_diff_right_inj
 
-@[simp] lemma symm_diff_eq_right : a Δ b = b ↔ a = ⊥ := by rw [symm_diff_comm, symm_diff_eq_left]
+@[simp] lemma symm_diff_eq_right : a ∆ b = b ↔ a = ⊥ := by rw [symm_diff_comm, symm_diff_eq_left]
 
-@[simp] lemma symm_diff_eq_bot : a Δ b = ⊥ ↔ a = b :=
-calc a Δ b = ⊥ ↔ a Δ b = a Δ a : by rw symm_diff_self
+@[simp] lemma symm_diff_eq_bot : a ∆ b = ⊥ ↔ a = b :=
+calc a ∆ b = ⊥ ↔ a ∆ b = a ∆ a : by rw symm_diff_self
            ... ↔     a = b     : by rw [symm_diff_right_inj, eq_comm]
 
-@[simp] lemma symm_diff_symm_diff_inf : a Δ b Δ (a ⊓ b) = a ⊔ b :=
+@[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 :=
+@[simp] lemma inf_symm_diff_symm_diff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b :=
 by rw [symm_diff_comm, symm_diff_symm_diff_inf]
 
 variables {a b c}
 
 protected lemma disjoint.symm_diff_left (ha : disjoint a c) (hb : disjoint b c) :
-  disjoint (a Δ b) c :=
+  disjoint (a ∆ b) c :=
 by { rw symm_diff_eq_sup_sdiff_inf, exact (ha.sup_left hb).disjoint_sdiff_left }
 
 protected lemma disjoint.symm_diff_right (ha : disjoint a b) (hb : disjoint a c) :
-  disjoint a (b Δ c) :=
+  disjoint a (b ∆ c) :=
 (ha.symm.symm_diff_left hb.symm).symm
 
 end generalized_boolean_algebra
 
 section boolean_algebra
 variables {α : Type*} [boolean_algebra α] (a b c : α)
 
-lemma symm_diff_eq : a Δ b = (a ⊓ bᶜ) ⊔ (b ⊓ aᶜ) := by simp only [(Δ), sdiff_eq]
+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]
+@[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 compl_symm_diff : (a Δ b)ᶜ = (a ⊓ b) ⊔ (aᶜ ⊓ bᶜ) :=
+lemma compl_symm_diff : (a ∆ b)ᶜ = (a ⊓ b) ⊔ (aᶜ ⊓ bᶜ) :=
 by simp only [←top_sdiff, sdiff_symm_diff, top_inf_eq]
 
-lemma symm_diff_eq_top_iff : a Δ b = ⊤ ↔ is_compl a b :=
+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
+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 = ⊤ :=
+@[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 symm_diff_compl_self : a ∆ aᶜ = ⊤ := by rw [symm_diff_comm, compl_symm_diff_self]
 
 lemma symm_diff_symm_diff_right' :
-  a Δ (b Δ c) = (a ⊓ b ⊓ c) ⊔ (a ⊓ bᶜ ⊓ cᶜ) ⊔ (aᶜ ⊓ b ⊓ cᶜ) ⊔ (aᶜ ⊓ bᶜ ⊓ c) :=
-calc a Δ (b Δ c) = (a ⊓ ((b ⊓ c) ⊔ (bᶜ ⊓ cᶜ))) ⊔
+  a ∆ (b ∆ c) = (a ⊓ b ⊓ c) ⊔ (a ⊓ bᶜ ⊓ cᶜ) ⊔ (aᶜ ⊓ b ⊓ cᶜ) ⊔ (aᶜ ⊓ bᶜ ⊓ c) :=
+calc a ∆ (b ∆ c) = (a ⊓ ((b ⊓ c) ⊔ (bᶜ ⊓ cᶜ))) ⊔
                      (((b ⊓ cᶜ) ⊔ (c ⊓ bᶜ)) ⊓ aᶜ)  : by rw [symm_diff_eq, compl_symm_diff,
                                                             symm_diff_eq]
              ... = (a ⊓ b ⊓ c) ⊔ (a ⊓ bᶜ ⊓ cᶜ) ⊔