restrict — Mathlib

English

Suppose φ is an almost-everywhere cover. For any measurable set s, restricting μ to s yields an almost-everywhere cover by φ i ∩ s.

Русский

Пусть φ образует покрытие почти всюду. При любом измеримом множестве s пересечение φ i с s образует тоже покрытие почти всюду относительно меры μ.restrict s.

LaTeX

$$$\mathrm{AECover}(\mu, l, \phi) \Rightarrow \mathrm{AECover}(\mu\restriction s, l, i \mapsto \phi(i) \cap s),$ при условии что s измеримо.$$

Lean4

protected theorem restrict {φ : ι → Set α} (hφ : AECover μ l φ) {s : Set α} : AECover (μ.restrict s) l φ :=
  hφ.mono Measure.restrict_le_self

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