{α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace 𝕜 F] →
            MeasurableSpace α →
              [inst_3 : MeasurableSpace α] →
                (p : ENNReal) → (μ : MeasureTheory.Measure α) → Submodule 𝕜 ↥(MeasureTheory.Lp F p μ)