restrict_measure_eq — Mathlib

English

The underlying measure of the restricted finite measure equals the restriction of the underlying measure: (μ.restrict A).toMeasure = μ.toMeasure.restrict A.

Русский

Базовая мера ограниченной конечной меры равна ограничению базовой меры: (μ.restrict A).toMeasure = μ.toMeasure.restrict A.

LaTeX

$$$ (\mu.restrict A).toMeasure = (\mu.toMeasure).restrict A $$$

Lean4

theorem restrict_measure_eq (μ : FiniteMeasure Ω) (A : Set Ω) :
    (μ.restrict A : Measure Ω) = (μ : Measure Ω).restrict A :=
  rfl

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