restrict — Mathlib

English

Restrict an OuterMeasure m to a set s, resulting in an outer measure on the same space defined by (restrict s m)(t) = m(t ∩ s).

Русский

Ограничение внешней меры m до множества s даёт новую внешнюю меру на той же пространстве: (restrict s m)(t) = m(t ∩ s).

LaTeX

$$$ (\restrict\ s\ m)(T) = m(T \cap s) $$$

Lean4

/-- Restrict an `OuterMeasure` to a set. -/
def restrict (s : Set α) : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure α :=
  (map (↑)).comp
    (comap ((↑) : s → α))
      -- TODO (kmill): change `m (t ∩ s)` to `m (s ∩ t)`

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