If an Lp space is complete, so is the target space

theorem MeasureTheory.FinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {mα : MeasurableSpace α} {μ : Measure α} {f : α → E} (hf : FinStronglyMeasurable f μ) (h'f : ¬f =ᵐ[μ] 0) : ∃ (s : Set α), MeasurableSet s ∧ 0 < μ s ∧ μ s < ⊤

theorem MeasureTheory.AEFinStronglyMeasurable.exists_measurableSet_measure_pos_lt_top {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {mα : MeasurableSpace α} {μ : Measure α} {f : α → E} (hf : AEFinStronglyMeasurable f μ) (h'f : ¬f =ᵐ[μ] 0) : ∃ (s : Set α), MeasurableSet s ∧ 0 < μ s ∧ μ s < ⊤

theorem MeasureTheory.nontrivial_Lp_real_of_nontrivial_Lp {α : Type u_1} (E : Type u_2) [NormedAddCommGroup E] {mα : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [Nontrivial ↥(Lp E p μ)] : Nontrivial ↥(Lp ℝ p μ)

theorem MeasureTheory.completeSpace_of_completeSpace_Lp {α : Type u_1} (E : Type u_2) [NormedAddCommGroup E] {mα : MeasurableSpace α} (p : ENNReal) (μ : Measure α) [NormedSpace ℝ E] [hp : Fact (1 ≤ p)] [CompleteSpace ↥(Lp E p μ)] [Nontrivial ↥(Lp E p μ)] : CompleteSpace E

If an L^p space is complete and nontrivial, then the target space is complete.