English
Restriction to a union of sets distributes over iUnion: v ≤[⋃ f n] w if v ≤[f n] w for all n with measurability.
Русский
Ограничение до объединения множеств распределяется по iUnion: v ≤[⋃ f n] w если v ≤[f n] w для всех n и каждый f n измерим.
LaTeX
$$$ v \\le[⋃ n, f n] w $$$
Lean4
theorem restrict_le_restrict_iUnion {f : ℕ → Set α} (hf₁ : ∀ n, MeasurableSet (f n)) (hf₂ : ∀ n, v ≤[f n] w) :
v ≤[⋃ n, f n] w := by
refine restrict_le_restrict_of_subset_le v w fun a ha₁ ha₂ => ?_
have ha₃ : ⋃ n, a ∩ disjointed f n = a := by rwa [← Set.inter_iUnion, iUnion_disjointed, Set.inter_eq_left]
have ha₄ : Pairwise (Disjoint on fun n => a ∩ disjointed f n) :=
(disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
rw [← ha₃, v.of_disjoint_iUnion _ ha₄, w.of_disjoint_iUnion _ ha₄]
· refine Summable.tsum_le_tsum (fun n => (restrict_le_restrict_iff v w (hf₁ n)).1 (hf₂ n) ?_ ?_) ?_ ?_
· exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
· exact Set.Subset.trans Set.inter_subset_right (disjointed_subset _ _)
· refine (v.m_iUnion (fun n => ?_) ?_).summable
· exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
· exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
· refine (w.m_iUnion (fun n => ?_) ?_).summable
· exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
· exact (disjoint_disjointed _).mono fun i j => Disjoint.mono inf_le_right inf_le_right
· intro n
exact ha₁.inter (MeasurableSet.disjointed hf₁ n)
· exact fun n => ha₁.inter (MeasurableSet.disjointed hf₁ n)
