countable_meas_level_set_pos₀ — Mathlib

English

For a measurable g: α → β, the set of level values t ∈ β for which μ({a ∈ α : g(a) = t}) > 0 is countable.

Русский

Для измеримой функции g: α → β множество значений уровня t ∈ β, для которых μ({a ∈ α : g(a) = t}) > 0, счётно.

LaTeX

$$countable {t : β | 0 < μ {a : α | g(a) = t}}$$

Lean4

theorem countable_meas_level_set_pos₀ {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SFinite μ]
    [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β} (g_mble : NullMeasurable g μ) :
    Set.Countable {t : β | 0 < μ {a : α | g a = t}} :=
  by
  have level_sets_disjoint : Pairwise (Disjoint on fun t : β => {a : α | g a = t}) := fun s t hst =>
    Disjoint.preimage g (disjoint_singleton.mpr hst)
  exact
    Measure.countable_meas_pos_of_disjoint_iUnion₀
      (fun b => g_mble (‹MeasurableSingletonClass β›.measurableSet_singleton b))
      ((fun _ _ h ↦ Disjoint.aedisjoint (level_sets_disjoint h)))

Похожие утверждения