Theorems · Definition · measure theory

MeasureTheory.IsTightMeasureSet

{𝓧 : Type u_1} → {m𝓧 : MeasurableSpace 𝓧} → [TopologicalSpace 𝓧] → Set (MeasureTheory.Measure 𝓧) → Prop

A set of measures S is tight if for all 0 < ε, there exists a compact set K such that for all μ ∈ S, μ Kᶜ ≤ ε. This is formulated in terms of filters, and proven equivalent to the definition above in IsTightMeasureSet_iff_exists_isCompact_measure_compl_le.

Defined in

Mathlib.MeasureTheory.Measure.Tight

Cited by

31 results in Mathlib

Foundations

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

Assumes

TopologicalSpace