restrict_apply — Mathlib

English

The restricted measure μ.restrict A assigns to s the same value as μ does to s ∩ A, for measurable s.

Русский

Ограниченная мера μ.restrict A присваивает s такое же значение, что и μ для s ∩ A, если s измеримо.

LaTeX

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

Lean4

theorem restrict_apply (μ : FiniteMeasure Ω) (A : Set Ω) {s : Set Ω} (s_mble : MeasurableSet s) :
    (μ.restrict A) s = μ (s ∩ A) := by
  apply congr_arg ENNReal.toNNReal
  exact Measure.restrict_apply s_mble

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