measure_if — Mathlib

English

On a countable space, two measures are equal if they agree on all measurable atoms.

Русский

На счётном пространстве две меры равны, если они совпадают на всех измеримых атомах.

LaTeX

$$$$\text{If } \alpha\text{ is countable and } \forall x,\ \mu(\text{measurableAtom}(x)) = \nu(\text{measurableAtom}(x)) \text{ then } \mu = \nu.$$$$

Lean4

theorem measure_if {x : β} {t : Set β} {s : Set α} [Decidable (x ∈ t)] :
    μ (if x ∈ t then s else ∅) = indicator t (fun _ => μ s) x := by split_ifs with h <;> simp [h]

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