measurableSet_pi_of_nonempty — Mathlib

English

If s is countable and pi(s,t) is nonempty, then MeasurableSet(pi(s,t)) is equivalent to ∀ i ∈ s, MeasurableSet(t(i)).

Русский

Если s счётно и pi(s,t) непусто, то MeasurableSet(pi(s,t)) эквивалентно ∀ i ∈ s, MeasurableSet(t(i)).

LaTeX

$$$\\text{MeasurableSet}(\\pi s t) \\iff \\forall i \\in s, \\text{MeasurableSet}(t i)$$$

Lean4

theorem measurableSet_pi_of_nonempty {s : Set δ} {t : ∀ i, Set (X i)} (hs : s.Countable) (h : (pi s t).Nonempty) :
    MeasurableSet (pi s t) ↔ ∀ i ∈ s, MeasurableSet (t i) := by
  classical
  rcases h with ⟨f, hf⟩
  refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩
  convert measurable_update f (a := i) hst
  rw [update_preimage_pi hi]
  exact fun j hj _ => hf j hj

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