theorem integration_properties {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} : (∀ (f : α → ℝ), 0 ≤ᵐ[μ] f → 0 ≤ ∫ (x : α), f x ∂μ) ∧ (∀ (f g : α → ℝ) (a b : ℝ), MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → ∫ (x : α), a • f x + b • g x ∂μ = a • ∫ (x : α), f x ∂μ + b • ∫ (x : α), g x ∂μ) ∧ (∀ (f g : α → ℝ), MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ) ∧ (∀ (f g : α → ℝ), f =ᵐ[μ] g → ∫ (x : α), f x ∂μ = ∫ (x : α), g x ∂μ) ∧ ∀ (f : α → ℝ), ‖∫ (x : α), f x ∂μ‖ ≤ ∫ (x : α), ‖f x‖ ∂μ

Basic properties of the Lebesgue (Bochner) integral. Bundles the five standard facts about integration of real-valued functions against a measure μ:

1. Positivity: if f ≥ 0 a.e. then ∫ f dμ ≥ 0.
2. Linearity: for integrable f, g and real scalars a, b, ∫ (a·f + b·g) dμ = a·∫ f dμ + b·∫ g dμ.
3. Monotonicity: if f ≤ g a.e. (both integrable) then ∫ f dμ ≤ ∫ g dμ.
4. a.e. congruence: if f = g a.e. then ∫ f dμ = ∫ g dμ.
5. Triangle inequality: |∫ f dμ| ≤ ∫ |f| dμ.