Theorems · Theorem · measure theory

MeasureTheory.OuterMeasure.trim_binop

∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ m₃ : MeasureTheory.OuterMeasure α}
  {op : ENNReal → ENNReal → ENNReal},
  (∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)) → ∀ (s : Set α), m₁.trim s = op (m₂.trim s) (m₃.trim s)

If m₁ s = op (m₂ s) (m₃ s) for all s, then the same is true for m₁.trim, m₂.trim, and m₃ s.

Defined in

Mathlib.MeasureTheory.OuterMeasure.Induced

Cited by

3 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace