English
Restrict a finite measure μ to a set A; the restricted finite measure μ.restrict A is defined by its underlying measure as (μ.restrict A).val = μ.restrict A and is indeed finite.
Русский
Ограничение конечной меры μ к множеству A: ограниченная мера μ.restrict A определяется через ограничение базовой меры μ и является конечной мерой.
LaTeX
$$$ (\mu.restrict A).toMeasure = (\mu.toMeasure).restrict A $$$
Lean4
/-- Restrict a finite measure μ to a set A. -/
def restrict (μ : FiniteMeasure Ω) (A : Set Ω) : FiniteMeasure Ω
where
val := (μ : Measure Ω).restrict A
property := MeasureTheory.isFiniteMeasureRestrict (μ : Measure Ω) A