restrict_le_restrict_countable_iUnion

English

If β is countable and f: β → Set α with each f b measurable and v ≤[f b] w for all b, then v ≤[⋃ b, f b] w.

Русский

Если β счётно, и f: β → Set α, все f b измеримы и v ≤[f b] w для всех b, то v ≤[⋃ b, f b] w.

LaTeX

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

Lean4

theorem restrict_le_restrict_countable_iUnion [Countable β] {f : β → Set α} (hf₁ : ∀ b, MeasurableSet (f b))
    (hf₂ : ∀ b, v ≤[f b] w) : v ≤[⋃ b, f b] w :=
  by
  cases nonempty_encodable β
  rw [← Encodable.iUnion_decode₂]
  refine restrict_le_restrict_iUnion v w ?_ ?_
  · intro n
    measurability
  · intro n
    rcases Encodable.decode₂ β n with - | b
    · simp
    · simp [hf₂ b]

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