English
For a finite index set s, μ|_{⋃_{i∈s} t_i} = ν|_{⋃_{i∈s} t_i} iff ∀ i ∈ s, μ|_{t_i} = ν|_{t_i}.
Русский
Для конечного множества индексов s: μ|_{⋃_{i∈s} t_i} = ν|_{⋃_{i∈s} t_i} тогда и только тогда, когда ∀ i ∈ s, μ|_{t_i} = ν|_{t_i}.
LaTeX
$$$\forall {s : Finset ι} \{t : ι → Set α\},\; μ.restrict (\bigcup i ∈ s, t i) = ν.restrict (\bigcup i ∈ s, t i) \iff \forall i ∈ s, μ.restrict (t i) = ν.restrict (t i)$$$
Lean4
/-- If two measures agree on all measurable subsets of `s` and `t`, then they agree on all
measurable subsets of `s ∪ t`. -/
theorem restrict_union_congr :
μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t :=
by
refine ⟨fun h ↦ ⟨restrict_congr_mono subset_union_left h, restrict_congr_mono subset_union_right h⟩, ?_⟩
rintro ⟨hs, ht⟩
ext1 u hu
simp only [restrict_apply hu, inter_union_distrib_left]
rcases exists_measurable_superset₂ μ ν (u ∩ s) with ⟨US, hsub, hm, hμ, hν⟩
calc
μ (u ∩ s ∪ u ∩ t) = μ (US ∪ u ∩ t) := measure_union_congr_of_subset hsub hμ.le Subset.rfl le_rfl
_ = μ US + μ ((u ∩ t) \ US) := (measure_add_diff hm.nullMeasurableSet _).symm
_ = restrict μ s u + restrict μ t (u \ US) := by
simp only [restrict_apply, hu, hu.diff hm, hμ, ← inter_comm t, inter_diff_assoc]
_ = restrict ν s u + restrict ν t (u \ US) := by rw [hs, ht]
_ = ν US + ν ((u ∩ t) \ US) := by simp only [restrict_apply, hu, hu.diff hm, hν, ← inter_comm t, inter_diff_assoc]
_ = ν (US ∪ u ∩ t) := (measure_add_diff hm.nullMeasurableSet _)
_ = ν (u ∩ s ∪ u ∩ t) := .symm <| measure_union_congr_of_subset hsub hν.le Subset.rfl le_rfl
