restrictₗ_apply — Mathlib

English

The linear restriction operator applied to μ equals the ordinary restricted measure: restricting via the linear map coincides with μ|s.

Русский

Линейный оператор ограничения, применённый к μ, равен обычному ограничению: ограничение через линейное отображение совпадает с μ|s.

LaTeX

$$$\text{restrict}_{\ell}(s)\, μ = μ\restriction s.$$$

Lean4

@[simp]
theorem restrictₗ_apply {_m0 : MeasurableSpace α} (s : Set α) (μ : Measure α) : restrictₗ s μ = μ.restrict s :=
  rfl

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