restrict_le_restrict_union — Mathlib

English

Same as above in a countable-indexed union setting; v ≤[⋃ b, f b] w when f is measurable and v ≤[f b] w for all b.

Русский

То же самое для объединения по счётному индексу; v ≤[⋃ b, f b] w при измеримости каждого f b и при v ≤[f b] w для всех b.

LaTeX

$$$ v \\le[\\bigcup_{b} f(b)] w $$$

Lean4

theorem restrict_le_restrict_union (hi₁ : MeasurableSet i) (hi₂ : v ≤[i] w) (hj₁ : MeasurableSet j) (hj₂ : v ≤[j] w) :
    v ≤[i ∪ j] w := by
  rw [Set.union_eq_iUnion]
  refine restrict_le_restrict_countable_iUnion v w ?_ ?_
  · measurability
  · rintro (_ | _) <;> simpa

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