inter_restrict — Mathlib

English

Same as inter_restrict, restated for emphasis.

Русский

То же самое, повторно для ясности.

LaTeX

$$$\mathrm{AECover}(\mu, l, \phi) \Rightarrow \mathrm{AECover}(\mu\restriction s, l, i \mapsto \phi(i) \cap s).$$$

Lean4

theorem inter_restrict {φ : ι → Set α} (hφ : AECover μ l φ) {s : Set α} (hs : MeasurableSet s) :
    AECover (μ.restrict s) l fun i => φ i ∩ s :=
  aecover_restrict_of_ae_imp hs (hφ.ae_eventually_mem.mono fun _x hx hxs => hx.mono fun _i hi => ⟨hi, hxs⟩) fun i =>
    (hφ.measurableSet i).inter hs

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