Theorems · Theorem · measure theory

MeasureTheory.addContent_mono

∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C} [inst_1 : PartialOrder G] [CanonicallyOrderedAdd G],
  MeasureTheory.IsSetSemiring C → s ∈ C → t ∈ C → s ⊆ t → m s ≤ m t

An addContent C on a SetSemiring C is monotone.

Defined in

Mathlib.MeasureTheory.Measure.AddContent

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderCanonicallyOrderedAdd