I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having difficulty with the notation. I struggle to find the correct file to "start" with when reading a new part of Mathlib, so I typically tend to find something that seems sufficiently basic which I want to learn about and start tracing dependencies. (If anyone has a better way, please help me...) I'm struggling to understand some of the notation I'm finding. For example, go to MeasureTheory/Integral/SetToL1.lean. We find the code
/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[𝕜] F`. -/
def setToL1SCLM' {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) : (α →₁ₛ[μ] E) →L[𝕜] F :=
LinearMap.mkContinuous
⟨⟨setToL1S T, setToL1S_add T (fun _ => hT.eq_zero_of_measure_zero) hT.1⟩,
setToL1S_smul T (fun _ => hT.eq_zero_of_measure_zero) hT.1 h_smul⟩
C fun f => norm_setToL1S_le T hT.2 f
Take E →L[ℝ] F, for instance, though I could have chosen quite a few examples. When I hover over it, it calls itself a continuous map between modules, but doesn't give a location in Mathlib to find this explanation. Needless to say
/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[𝕜] F`. -/
means nothing to me right now. Hence: Is there a "nice" path through which to explore Mathlib/MeasureTheory?
