refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICUL…

…AR instead of ⊥ UP TACK (#18423)

The previous notation for `measure_theory.measure.mutually_singular` was `⊥ₘ`. This changes it to `⟂ₘ`, which is semantically a better character.

The same change is made for `measure_theory.vector_measure.mutually_singular`, from `⊥ᵥ` to `⟂ᵥ`.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Perpendicular.20notation/near/327158463)

src/measure_theory/covering/differentiation.lean

@@ -158,7 +158,7 @@ variables [second_countable_topology α] [borel_space α] [is_locally_finite_mea
 /-- If a measure `ρ` is singular with respect to `μ`, then for `μ` almost every `x`, the ratio
 `ρ a / μ a` tends to zero when `a` shrinks to `x` along the Vitali family. This makes sense
 as `μ a` is eventually positive by `ae_eventually_measure_pos`. -/
-lemma ae_eventually_measure_zero_of_singular (hρ : ρ ⊥ₘ μ) :
+lemma ae_eventually_measure_zero_of_singular (hρ : ρ ⟂ₘ μ) :
   ∀ᵐ x ∂μ, tendsto (λ a, ρ a / μ a) (v.filter_at x) (𝓝 0) :=
 begin
   have A : ∀ ε > (0 : ℝ≥0), ∀ᵐ x ∂μ, ∀ᶠ a in v.filter_at x, ρ a < ε * μ a,

src/measure_theory/decomposition/jordan.lean

@@ -52,7 +52,7 @@ finite measures. -/
 (pos_part neg_part : measure α)
 [pos_part_finite : is_finite_measure pos_part]
 [neg_part_finite : is_finite_measure neg_part]
-(mutually_singular : pos_part ⊥ₘ neg_part)
+(mutually_singular : pos_part ⟂ₘ neg_part)
 
 attribute [instance] jordan_decomposition.pos_part_finite
 attribute [instance] jordan_decomposition.neg_part_finite
@@ -510,7 +510,7 @@ end
 
 -- TODO: Generalize to vector measures once total variation on vector measures is defined
 lemma mutually_singular_iff (s t : signed_measure α) :
-  s ⊥ᵥ t ↔ s.total_variation ⊥ₘ t.total_variation :=
+  s ⟂ᵥ t ↔ s.total_variation ⟂ₘ t.total_variation :=
 begin
   split,
   { rintro ⟨u, hmeas, hu₁, hu₂⟩,
@@ -531,7 +531,7 @@ begin
 end
 
 lemma mutually_singular_ennreal_iff (s : signed_measure α) (μ : vector_measure α ℝ≥0∞) :
-  s ⊥ᵥ μ ↔ s.total_variation ⊥ₘ μ.ennreal_to_measure :=
+  s ⟂ᵥ μ ↔ s.total_variation ⟂ₘ μ.ennreal_to_measure :=
 begin
   split,
   { rintro ⟨u, hmeas, hu₁, hu₂⟩,
@@ -550,8 +550,8 @@ begin
 end
 
 lemma total_variation_mutually_singular_iff (s : signed_measure α) (μ : measure α) :
-  s.total_variation ⊥ₘ μ ↔
-  s.to_jordan_decomposition.pos_part ⊥ₘ μ ∧ s.to_jordan_decomposition.neg_part ⊥ₘ μ :=
+  s.total_variation ⟂ₘ μ ↔
+  s.to_jordan_decomposition.pos_part ⟂ₘ μ ∧ s.to_jordan_decomposition.neg_part ⟂ₘ μ :=
 measure.mutually_singular.add_left_iff
 
 end signed_measure

src/measure_theory/decomposition/lebesgue.lean

@@ -74,7 +74,7 @@ measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular
 `ν` and `μ = ξ + ν.with_density f`. -/
 class have_lebesgue_decomposition (μ ν : measure α) : Prop :=
 (lebesgue_decomposition :
-  ∃ (p : measure α × (α → ℝ≥0∞)), measurable p.2 ∧ p.1 ⊥ₘ ν ∧ μ = p.1 + ν.with_density p.2)
+  ∃ (p : measure α × (α → ℝ≥0∞)), measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.with_density p.2)
 
 /-- If a pair of measures `have_lebesgue_decomposition`, then `singular_part` chooses the
 measure from `have_lebesgue_decomposition`, otherwise it returns the zero measure. For sigma-finite
@@ -92,7 +92,7 @@ if h : have_lebesgue_decomposition μ ν then (classical.some h.lebesgue_decompo
 
 lemma have_lebesgue_decomposition_spec (μ ν : measure α)
   [h : have_lebesgue_decomposition μ ν] :
-  measurable (μ.rn_deriv ν) ∧ (μ.singular_part ν) ⊥ₘ ν ∧
+  measurable (μ.rn_deriv ν) ∧ (μ.singular_part ν) ⟂ₘ ν ∧
   μ = (μ.singular_part ν) + ν.with_density (μ.rn_deriv ν) :=
 begin
   rw [singular_part, rn_deriv, dif_pos h, dif_pos h],
@@ -129,7 +129,7 @@ begin
 end
 
 lemma mutually_singular_singular_part (μ ν : measure α) :
-  μ.singular_part ν ⊥ₘ ν :=
+  μ.singular_part ν ⟂ₘ ν :=
 begin
   by_cases h : have_lebesgue_decomposition μ ν,
   { exactI (have_lebesgue_decomposition_spec μ ν).2.1 },
@@ -226,7 +226,7 @@ This theorem provides the uniqueness of the `singular_part` in the Lebesgue deco
 while `measure_theory.measure.eq_rn_deriv` provides the uniqueness of the
 `rn_deriv`. -/
 theorem eq_singular_part {s : measure α} {f : α → ℝ≥0∞} (hf : measurable f)
-  (hs : s ⊥ₘ ν) (hadd : μ = s + ν.with_density f) :
+  (hs : s ⟂ₘ ν) (hadd : μ = s + ν.with_density f) :
   s = μ.singular_part ν :=
 begin
   haveI : have_lebesgue_decomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩,
@@ -316,7 +316,7 @@ theorem, while `measure_theory.measure.eq_singular_part` provides the uniqueness
 `singular_part`. Here, the uniqueness is given in terms of the measures, while the uniqueness in
 terms of the functions is given in `eq_rn_deriv`. -/
 theorem eq_with_density_rn_deriv {s : measure α} {f : α → ℝ≥0∞} (hf : measurable f)
-  (hs : s ⊥ₘ ν) (hadd : μ = s + ν.with_density f) :
+  (hs : s ⟂ₘ ν) (hadd : μ = s + ν.with_density f) :
   ν.with_density f = ν.with_density (μ.rn_deriv ν) :=
 begin
   haveI : have_lebesgue_decomposition μ ν := ⟨⟨⟨s, f⟩, hf, hs, hadd⟩⟩,
@@ -366,7 +366,7 @@ theorem, while `measure_theory.measure.eq_singular_part` provides the uniqueness
 `singular_part`. Here, the uniqueness is given in terms of the functions, while the uniqueness in
 terms of the functions is given in `eq_with_density_rn_deriv`. -/
 theorem eq_rn_deriv [sigma_finite ν] {s : measure α} {f : α → ℝ≥0∞} (hf : measurable f)
-  (hs : s ⊥ₘ ν) (hadd : μ = s + ν.with_density f) :
+  (hs : s ⟂ₘ ν) (hadd : μ = s + ν.with_density f) :
   f =ᵐ[ν] μ.rn_deriv ν :=
 begin
   refine ae_eq_of_forall_set_lintegral_eq_of_sigma_finite hf (measurable_rn_deriv μ ν) _,
@@ -400,7 +400,7 @@ a measurable set `E`, such that `ν(E) > 0` and `E` is positive with respect to
 
 This lemma is useful for the Lebesgue decomposition theorem. -/
 lemma exists_positive_of_not_mutually_singular
-  (μ ν : measure α) [is_finite_measure μ] [is_finite_measure ν] (h : ¬ μ ⊥ₘ ν) :
+  (μ ν : measure α) [is_finite_measure μ] [is_finite_measure ν] (h : ¬ μ ⟂ₘ ν) :
   ∃ ε : ℝ≥0, 0 < ε ∧ ∃ E : set α, measurable_set E ∧ 0 < ν E ∧
   0 ≤[E] μ.to_signed_measure - (ε • ν).to_signed_measure :=
 begin
@@ -704,7 +704,7 @@ instance have_lebesgue_decomposition_of_sigma_finite
   { choose A hA₁ hA₂ hA₃ using λ n, mutually_singular_singular_part (μn n) (νn n),
     simp only [hξ],
   -- We use the set `B := ⋃ j, (S.set j) ∩ A j` where `A n` is the set provided as
-  -- `singular_part (μn n) (νn n) ⊥ₘ νn n`
+  -- `singular_part (μn n) (νn n) ⟂ₘ νn n`
     refine ⟨⋃ j, (S.set j) ∩ A j,
       measurable_set.Union (λ n, (S.set_mem n).inter (hA₁ n)), _, _⟩,
   -- `ξ B = 0` since `ξ B = ∑ i j, singular_part (μn j) (νn j) (S.set i ∩ A i)`
@@ -855,7 +855,7 @@ def singular_part (s : signed_measure α) (μ : measure α) : signed_measure α
 section
 
 lemma singular_part_mutually_singular (s : signed_measure α) (μ : measure α) :
-  s.to_jordan_decomposition.pos_part.singular_part μ ⊥ₘ
+  s.to_jordan_decomposition.pos_part.singular_part μ ⟂ₘ
   s.to_jordan_decomposition.neg_part.singular_part μ :=
 begin
   by_cases hl : s.have_lebesgue_decomposition μ,
@@ -888,10 +888,10 @@ begin
 end
 
 lemma mutually_singular_singular_part (s : signed_measure α) (μ : measure α) :
-  singular_part s μ ⊥ᵥ μ.to_ennreal_vector_measure :=
+  singular_part s μ ⟂ᵥ μ.to_ennreal_vector_measure :=
 begin
   rw [mutually_singular_ennreal_iff, singular_part_total_variation],
-  change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ),
+  change _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ),
   rw vector_measure.equiv_measure.right_inv μ,
   exact (mutually_singular_singular_part _ _).add_left (mutually_singular_singular_part _ _)
 end
@@ -958,13 +958,13 @@ end
 variables {s μ}
 
 lemma jordan_decomposition_add_with_density_mutually_singular
-  {f : α → ℝ} (hf : measurable f) (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) :
-  t.to_jordan_decomposition.pos_part + μ.with_density (λ (x : α), ennreal.of_real (f x)) ⊥ₘ
+  {f : α → ℝ} (hf : measurable f) (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) :
+  t.to_jordan_decomposition.pos_part + μ.with_density (λ (x : α), ennreal.of_real (f x)) ⟂ₘ
   t.to_jordan_decomposition.neg_part + μ.with_density (λ (x : α), ennreal.of_real (-f x)) :=
 begin
   rw [mutually_singular_ennreal_iff, total_variation_mutually_singular_iff] at htμ,
-  change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) ∧
-         _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
+  change _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) ∧
+         _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
   rw [vector_measure.equiv_measure.right_inv] at htμ,
   exact ((jordan_decomposition.mutually_singular _).add_right
     (htμ.1.mono_ac (refl _) (with_density_absolutely_continuous _ _))).add_left
@@ -974,7 +974,7 @@ end
 
 lemma to_jordan_decomposition_eq_of_eq_add_with_density
   {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   s.to_jordan_decomposition = @jordan_decomposition.mk α _
     (t.to_jordan_decomposition.pos_part + μ.with_density (λ x, ennreal.of_real (f x)))
     (t.to_jordan_decomposition.neg_part + μ.with_density (λ x, ennreal.of_real (- f x)))
@@ -1001,12 +1001,12 @@ end
 
 private lemma have_lebesgue_decomposition_mk' (μ : measure α)
   {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   s.have_lebesgue_decomposition μ :=
 begin
   have htμ' := htμ,
   rw mutually_singular_ennreal_iff at htμ,
-  change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
+  change _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
   rw [vector_measure.equiv_measure.right_inv, total_variation_mutually_singular_iff] at htμ,
   refine
     { pos_part :=
@@ -1020,7 +1020,7 @@ begin
 end
 
 lemma have_lebesgue_decomposition_mk (μ : measure α) {f : α → ℝ} (hf : measurable f)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   s.have_lebesgue_decomposition μ :=
 begin
   by_cases hfi : integrable f μ,
@@ -1032,13 +1032,13 @@ end
 
 private theorem eq_singular_part'
   (t : signed_measure α) {f : α → ℝ} (hf : measurable f) (hfi : integrable f μ)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   t = s.singular_part μ :=
 begin
   have htμ' := htμ,
   rw [mutually_singular_ennreal_iff, total_variation_mutually_singular_iff] at htμ,
-  change _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) ∧
-         _ ⊥ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
+  change _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) ∧
+         _ ⟂ₘ vector_measure.equiv_measure.to_fun (vector_measure.equiv_measure.inv_fun μ) at htμ,
   rw [vector_measure.equiv_measure.right_inv] at htμ,
   { rw [singular_part, ← t.to_signed_measure_to_jordan_decomposition,
         jordan_decomposition.to_signed_measure],
@@ -1056,7 +1056,7 @@ mutually singular with respect to `μ` and `s = t + μ.with_densityᵥ f`, we ha
 `t = singular_part s μ`, i.e. `t` is the singular part of the Lebesgue decomposition between
 `s` and `μ`. -/
 theorem eq_singular_part (t : signed_measure α) (f : α → ℝ)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   t = s.singular_part μ :=
 begin
   by_cases hfi : integrable f μ,
@@ -1139,7 +1139,7 @@ by { rw [sub_eq_add_neg, sub_eq_add_neg, singular_part_add, singular_part_neg] }
 mutually singular with respect to `μ` and `s = t + μ.with_densityᵥ f`, we have
 `f = rn_deriv s μ`, i.e. `f` is the Radon-Nikodym derivative of `s` and `μ`. -/
 theorem eq_rn_deriv (t : signed_measure α) (f : α → ℝ) (hfi : integrable f μ)
-  (htμ : t ⊥ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
+  (htμ : t ⟂ᵥ μ.to_ennreal_vector_measure) (hadd : s = t + μ.with_densityᵥ f) :
   f =ᵐ[μ] s.rn_deriv μ :=
 begin
   set f' := hfi.1.mk f,

src/measure_theory/integral/lebesgue.lean

@@ -2483,7 +2483,7 @@ lemma with_density_indicator_one {s : set α} (hs : measurable_set s) :
 by rw [with_density_indicator hs, with_density_one]
 
 lemma with_density_of_real_mutually_singular {f : α → ℝ} (hf : measurable f) :
-  μ.with_density (λ x, ennreal.of_real $ f x) ⊥ₘ μ.with_density (λ x, ennreal.of_real $ -f x) :=
+  μ.with_density (λ x, ennreal.of_real $ f x) ⟂ₘ μ.with_density (λ x, ennreal.of_real $ -f x) :=
 begin
   set S : set α := { x | f x < 0 } with hSdef,
   have hS : measurable_set S := measurable_set_lt hf measurable_const,

src/measure_theory/measure/mutually_singular.lean

@@ -8,9 +8,9 @@ import measure_theory.measure.measure_space
 /-! # Mutually singular measures
 
 Two measures `μ`, `ν` are said to be mutually singular (`measure_theory.measure.mutually_singular`,
-localized notation `μ ⊥ₘ ν`) if there exists a measurable set `s` such that `μ s = 0` and
+localized notation `μ ⟂ₘ ν`) if there exists a measurable set `s` such that `μ s = 0` and
 `ν sᶜ = 0`. The measurability of `s` is an unnecessary assumption (see
-`measure_theory.measure.mutually_singular.mk`) but we keep it because this way `rcases (h : μ ⊥ₘ ν)`
+`measure_theory.measure.mutually_singular.mk`) but we keep it because this way `rcases (h : μ ⟂ₘ ν)`
 gives us a measurable set and usually it is easy to prove measurability.
 
 In this file we define the predicate `measure_theory.measure.mutually_singular` and prove basic
@@ -36,7 +36,7 @@ def mutually_singular {m0 : measurable_space α} (μ ν : measure α) : Prop :=
 ∃ (s : set α), measurable_set s ∧ μ s = 0 ∧ ν sᶜ = 0
 
 localized "infix (name := measure.mutually_singular)
-  ` ⊥ₘ `:60 := measure_theory.measure.mutually_singular" in measure_theory
+  ` ⟂ₘ `:60 := measure_theory.measure.mutually_singular" in measure_theory
 
 namespace mutually_singular
 
@@ -48,23 +48,23 @@ begin
   exact subset_to_measurable _ _ hxs
 end
 
-@[simp] lemma zero_right : μ ⊥ₘ 0 := ⟨∅, measurable_set.empty, measure_empty, rfl⟩
+@[simp] lemma zero_right : μ ⟂ₘ 0 := ⟨∅, measurable_set.empty, measure_empty, rfl⟩
 
-@[symm] lemma symm (h : ν ⊥ₘ μ) : μ ⊥ₘ ν :=
+@[symm] lemma symm (h : ν ⟂ₘ μ) : μ ⟂ₘ ν :=
 let ⟨i, hi, his, hit⟩ := h in ⟨iᶜ, hi.compl, hit, (compl_compl i).symm ▸ his⟩
 
-lemma comm : μ ⊥ₘ ν ↔ ν ⊥ₘ μ := ⟨λ h, h.symm, λ h, h.symm⟩
+lemma comm : μ ⟂ₘ ν ↔ ν ⟂ₘ μ := ⟨λ h, h.symm, λ h, h.symm⟩
 
-@[simp] lemma zero_left : 0 ⊥ₘ μ := zero_right.symm
+@[simp] lemma zero_left : 0 ⟂ₘ μ := zero_right.symm
 
-lemma mono_ac (h : μ₁ ⊥ₘ ν₁) (hμ : μ₂ ≪ μ₁) (hν : ν₂ ≪ ν₁) : μ₂ ⊥ₘ ν₂ :=
+lemma mono_ac (h : μ₁ ⟂ₘ ν₁) (hμ : μ₂ ≪ μ₁) (hν : ν₂ ≪ ν₁) : μ₂ ⟂ₘ ν₂ :=
 let ⟨s, hs, h₁, h₂⟩ := h in ⟨s, hs, hμ h₁, hν h₂⟩
 
-lemma mono (h : μ₁ ⊥ₘ ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) : μ₂ ⊥ₘ ν₂ :=
+lemma mono (h : μ₁ ⟂ₘ ν₁) (hμ : μ₂ ≤ μ₁) (hν : ν₂ ≤ ν₁) : μ₂ ⟂ₘ ν₂ :=
 h.mono_ac hμ.absolutely_continuous hν.absolutely_continuous
 
 @[simp] lemma sum_left {ι : Type*} [countable ι] {μ : ι → measure α} :
-  (sum μ) ⊥ₘ ν ↔ ∀ i, μ i ⊥ₘ ν :=
+  (sum μ) ⟂ₘ ν ↔ ∀ i, μ i ⟂ₘ ν :=
 begin
   refine ⟨λ h i, h.mono (le_sum _ _) le_rfl, λ H, _⟩,
   choose s hsm hsμ hsν using H,
@@ -75,25 +75,25 @@ begin
 end
 
 @[simp] lemma sum_right {ι : Type*} [countable ι] {ν : ι → measure α} :
-  μ ⊥ₘ sum ν ↔ ∀ i, μ ⊥ₘ ν i :=
+  μ ⟂ₘ sum ν ↔ ∀ i, μ ⟂ₘ ν i :=
 comm.trans $ sum_left.trans $ forall_congr $ λ i, comm
 
-@[simp] lemma add_left_iff : μ₁ + μ₂ ⊥ₘ ν ↔ μ₁ ⊥ₘ ν ∧ μ₂ ⊥ₘ ν :=
+@[simp] lemma add_left_iff : μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν :=
 by rw [← sum_cond, sum_left, bool.forall_bool, cond, cond, and.comm]
 
-@[simp] lemma add_right_iff : μ ⊥ₘ ν₁ + ν₂ ↔ μ ⊥ₘ ν₁ ∧ μ ⊥ₘ ν₂ :=
+@[simp] lemma add_right_iff : μ ⟂ₘ ν₁ + ν₂ ↔ μ ⟂ₘ ν₁ ∧ μ ⟂ₘ ν₂ :=
 comm.trans $ add_left_iff.trans $ and_congr comm comm
 
-lemma add_left (h₁ : ν₁ ⊥ₘ μ) (h₂ : ν₂ ⊥ₘ μ) : ν₁ + ν₂ ⊥ₘ μ :=
+lemma add_left (h₁ : ν₁ ⟂ₘ μ) (h₂ : ν₂ ⟂ₘ μ) : ν₁ + ν₂ ⟂ₘ μ :=
 add_left_iff.2 ⟨h₁, h₂⟩
 
-lemma add_right (h₁ : μ ⊥ₘ ν₁) (h₂ : μ ⊥ₘ ν₂) : μ ⊥ₘ ν₁ + ν₂ :=
+lemma add_right (h₁ : μ ⟂ₘ ν₁) (h₂ : μ ⟂ₘ ν₂) : μ ⟂ₘ ν₁ + ν₂ :=
 add_right_iff.2 ⟨h₁, h₂⟩
 
-lemma smul (r : ℝ≥0∞) (h : ν ⊥ₘ μ) : r • ν ⊥ₘ μ :=
+lemma smul (r : ℝ≥0∞) (h : ν ⟂ₘ μ) : r • ν ⟂ₘ μ :=
 h.mono_ac (absolutely_continuous.rfl.smul r) absolutely_continuous.rfl
 
-lemma smul_nnreal (r : ℝ≥0) (h : ν ⊥ₘ μ) : r • ν ⊥ₘ μ := h.smul r
+lemma smul_nnreal (r : ℝ≥0) (h : ν ⟂ₘ μ) : r • ν ⟂ₘ μ := h.smul r
 
 end mutually_singular