Theorems · Definition · measure theory

MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE

{α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ ν : MeasureTheory.Measure α} → ν ≤ μ → {C : Set (Set α)} → μ.FiniteSpanningSetsIn C → ν.FiniteSpanningSetsIn C

Given measures μ, ν where ν ≤ μ, FiniteSpanningSetsIn.ofLe provides the induced FiniteSpanningSet with respect to ν from a FiniteSpanningSet with respect to μ.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Cited by

2 results in Mathlib

Foundations

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