chore(MeasureTheory/MeasurableSpace/Basic): change reference to file …

…in docs (#8230)

An nonexistent file is mentioned in the intro docs, it is changed to
refer to the correct file.

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -20,7 +20,7 @@ import Mathlib.Data.Set.UnionLift
 # Measurable spaces and measurable functions
 
 This file provides properties of measurable spaces and the functions and isomorphisms
-between them. The definition of a measurable space is in `MeasureTheory.MeasurableSpaceDef`.
+between them. The definition of a measurable space is in `MeasureTheory.MeasurableSpace.Defs`.
 
 A measurable space is a set equipped with a σ-algebra, a collection of
 subsets closed under complementation and countable union. A function