countable_meas_level_set_pos — Mathlib

English

If a set t is covered by a countable family of finite-measure sets, then μ(toMeasurable μ t ∩ s) = μ(t ∩ s) for any measurable s.

Русский

Если множество t покрыто счётной семейством множеств конечной меры, то для любого измеримого s верно μ(toMeasurable μ t ∩ s) = μ(t ∩ s).

LaTeX

$$$t \subseteq \bigcup_{n} v(n) \land \forall n, μ(t \cap v(n)) < ∞ \Rightarrow μ(toMeasurable(μ,t) \cap s) = μ(t \cap s)$$$

Lean4

theorem countable_meas_level_set_pos {α β : Type*} {_ : MeasurableSpace α} {μ : Measure α} [SFinite μ]
    [MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β} (g_mble : Measurable g) :
    Set.Countable {t : β | 0 < μ {a : α | g a = t}} :=
  countable_meas_level_set_pos₀ g_mble.nullMeasurable

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