restrict_apply_measure — Mathlib

English

For any measurable set s, the restricted measure μ.restrict A evaluates s by μ(s ∩ A).

Русский

Для любого измеримого множества s величина ограниченной меры μ.restrict A равна μ(s ∩ A).

LaTeX

$$$\forall s\ (s \text{ measurable})\; (\mu.restrict A)(s) = \mu(s \cap A)$$$

Lean4

theorem restrict_apply_measure (μ : FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) :
    (μ.restrict A : Measure Ω) s = (μ : Measure Ω) (s ∩ A) :=
  Measure.restrict_apply s_mble

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