theorem starRingEnd_div_mul_eq_norm {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {f : α → 𝕜} (x : α) : (starRingEnd 𝕜) (f x / ↑‖f x‖) * f x = ↑‖f x‖

theorem enorm_algebraMap' {𝕜 : Type u_1} (𝕜' : Type u_2) [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormOneClass 𝕜'] (x : 𝕜) : ‖(algebraMap 𝕜 𝕜') x‖ₑ = ‖x‖ₑ

theorem enorm_integral_norm_eq_integral_enorm {α : Type u_1} {𝕜 : Type u_2} [MeasurableSpace α] [RCLike 𝕜] {μ : MeasureTheory.Measure α} {f : α → 𝕜} (hf : MeasureTheory.Integrable f μ) : ‖∫ (x : α), ‖f x‖ ∂μ‖ₑ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

theorem enorm_integral_starRingEnd_mul_eq_lintegral_enorm {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → 𝕜} (hf : MeasureTheory.Integrable f μ) : ‖∫ (x : α), (starRingEnd 𝕜) (f x / ↑‖f x‖) * f x ∂μ‖ₑ = ∫⁻ (x : α), ‖f x‖ₑ ∂μ

theorem enorm_integral_mul_starRingEnd_comm {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → 𝕜} : ‖∫ (x : α), f x * (starRingEnd 𝕜) (g x) ∂μ‖ₑ = ‖∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ‖ₑ

theorem MeasureTheory.setIntegral_union_2 {X : Type u_1} {E : Type u_2} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} {s t : Set X} {μ : Measure X} (hst : Disjoint s t) (ht : MeasurableSet t) (hfst : IntegrableOn f (s ∪ t) μ) : ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ

theorem MeasureTheory.exists_ne_zero_of_setIntegral_ne_zero {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : Measure α} {f : α → E} {U : Set α} (hU : ∫ (u : α) in U, f u ∂μ ≠ 0) : ∃ u ∈ U, f u ≠ 0

theorem MeasureTheory.exists_ne_zero_of_integral_ne_zero {α : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] {μ : Measure α} {f : α → E} (h : ∫ (u : α), f u ∂μ ≠ 0) : ∃ (u : α), f u ≠ 0