feat(Probability/BorelCantelli): clarify documentation (#8527)

Some of the students from my Lean seminar got quite confused trying to find the Borel-Cantelli lemmas in Mathlib, because there is a file `Probability.Martingale.BorelCantelli` but neither of the Borel-Cantelli lemmas are in it! This PR adds cross-links between the documentation strings for the various files concerned. (There are no changes to actual code.)

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -565,8 +565,12 @@ theorem tendsto_measure_biInter_gt {ι : Type*} [LinearOrder ι] [TopologicalSpa
   filter_upwards [this] with r hr using lt_of_le_of_lt (measure_mono (hm _ _ hr.1 hr.2)) hn
 #align measure_theory.tendsto_measure_bInter_gt MeasureTheory.tendsto_measure_biInter_gt
 
-/-- One direction of the **Borel-Cantelli lemma**: if (sᵢ) is a sequence of sets such
-that `∑ μ sᵢ` is finite, then the limit superior of the `sᵢ` is a null set. -/
+/-- One direction of the **Borel-Cantelli lemma** (sometimes called the "*first* Borel-Cantelli
+lemma"): if (sᵢ) is a sequence of sets such that `∑ μ sᵢ` is finite, then the limit superior of the
+`sᵢ` is a null set.
+
+Note: for the *second* Borel-Cantelli lemma (applying to independent sets in a probability space),
+see `ProbabilityTheory.measure_limsup_eq_one`. -/
 theorem measure_limsup_eq_zero {s : ℕ → Set α} (hs : (∑' i, μ (s i)) ≠ ∞) :
     μ (limsup s atTop) = 0 := by
   -- First we replace the sequence `sₙ` with a sequence of measurable sets `tₙ ⊇ sₙ` of the same

Mathlib/Probability/BorelCantelli.lean

@@ -13,7 +13,7 @@ import Mathlib.Probability.Independence.Basic
 
 # The second Borel-Cantelli lemma
 
-This file contains the second Borel-Cantelli lemma which states that, given a sequence of
+This file contains the *second Borel-Cantelli lemma* which states that, given a sequence of
 independent sets `(sₙ)` in a probability space, if `∑ n, μ sₙ = ∞`, then the limsup of `sₙ` has
 measure 1. We employ a proof using Lévy's generalized Borel-Cantelli by choosing an appropriate
 filtration.
@@ -22,6 +22,8 @@ filtration.
 
 - `ProbabilityTheory.measure_limsup_eq_one`: the second Borel-Cantelli lemma.
 
+**Note**: for the *first Borel-Cantelli lemma*, which holds in general measure spaces (not only
+in probability spaces), see `MeasureTheory.measure_limsup_eq_zero`.
 -/
 
 

Mathlib/Probability/Martingale/BorelCantelli.lean

@@ -18,6 +18,10 @@ Borel-Cantelli lemmas. With this generalization, one can easily deduce the Borel
 by choosing appropriate filtrations. This file also contains the one sided martingale bound which
 is required to prove the generalized Borel-Cantelli.
 
+**Note**: the usual Borel-Cantelli lemmas are not in this file. See
+`MeasureTheory.measure_limsup_eq_zero` for the first (which does not depend on the results here),
+and `ProbabilityTheory.measure_limsup_eq_one` for the second (which does).
+
 ## Main results
 
 - `MeasureTheory.Submartingale.bddAbove_iff_exists_tendsto`: the one sided martingale bound: given