restrict — Mathlib

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

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