doc: add mutual references to doc strings of AEMeasurable and NullMeasurable (#32593)

Author: fpvandoorn

Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

@@ -401,7 +401,10 @@ function. We define this property, called `AEMeasurable f μ`. It's properties a
 variable {m : MeasurableSpace α} [MeasurableSpace β] {f g : α → β} {μ ν : Measure α}
 
 /-- A function is almost everywhere measurable if it coincides almost everywhere with a measurable
-function. -/
+function.
+
+A similar notion is `MeasureTheory.NullMeasurable`. That notion is equivalent to `AEMeasurable` if
+the σ-algebra on the codomain is countably generated, but weaker in general. -/
 @[fun_prop]
 def AEMeasurable {_m : MeasurableSpace α} (f : α → β) (μ : Measure α := by volume_tac) : Prop :=
   ∃ g : α → β, Measurable g ∧ f =ᵐ[μ] g

Mathlib/MeasureTheory/Measure/NullMeasurable.lean

@@ -377,7 +377,10 @@ section NullMeasurable
 variable [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {f : α → β} {μ : Measure α}
 
 /-- A function `f : α → β` is null measurable if the preimage of a measurable set is a null
-measurable set. -/
+measurable set.
+
+A similar notion is `AEMeasurable`. That notion is equivalent to `NullMeasurable` if
+the σ-algebra on the codomain is countably generated, but stronger in general. -/
 def NullMeasurable (f : α → β) (μ : Measure α := by volume_tac) : Prop :=
   ∀ ⦃s : Set β⦄, MeasurableSet s → NullMeasurableSet (f ⁻¹' s) μ