English
Let π be a family of pi-systems. If a fixed κ μ makes the π-families independent, then the sigma-algebra generated by the intersections over a finite set S remains independent of the pi-system at a new index a not in S.
Русский
Пусть π — семейство пи-систем. Если для κ μ эти семейства независимы, то сигма-алгебра, порожденная пересечениями по конечному множеству S, остаётся независимой от пи-системы на новый индекс a, не принадлежащий S.
LaTeX
$$$IndepSets\left(\ piiUnionInter(\pi, S)\right)\left(\pi(a)\right)\ κ\ μ$$$
Lean4
theorem piiUnionInter_of_notMem {π : ι → Set (Set Ω)} {a : ι} {S : Finset ι} (hp_ind : iIndepSets π κ μ) (haS : a ∉ S) :
IndepSets (piiUnionInter π S) (π a) κ μ :=
by
rintro t1 t2 ⟨s, hs_mem, ft1, hft1_mem, ht1_eq⟩ ht2_mem_pia
rw [Finset.coe_subset] at hs_mem
classical
let f := fun n => ite (n = a) t2 (ite (n ∈ s) (ft1 n) Set.univ)
have h_f_mem : ∀ n ∈ insert a s, f n ∈ π n := by
intro n hn_mem_insert
dsimp only [f]
rcases Finset.mem_insert.mp hn_mem_insert with hn_mem | hn_mem
· simp [hn_mem, ht2_mem_pia]
· grind
have h_f_mem_pi : ∀ n ∈ s, f n ∈ π n := fun x hxS => h_f_mem x (by simp [hxS])
have h_t1 : t1 = ⋂ n ∈ s, f n := by
suffices h_forall : ∀ n ∈ s, f n = ft1 n by grind
intro n hnS
have hn_ne_a : n ≠ a := by rintro rfl; exact haS (hs_mem hnS)
simp_rw [f, if_pos hnS, if_neg hn_ne_a]
have h_μ_t1 : ∀ᵐ a' ∂μ, κ a' t1 = ∏ n ∈ s, κ a' (f n) :=
by
filter_upwards [hp_ind s h_f_mem_pi] with a' ha'
rw [h_t1, ← ha']
have h_t2 : t2 = f a := by simp [f]
have h_μ_inter : ∀ᵐ a' ∂μ, κ a' (t1 ∩ t2) = ∏ n ∈ insert a s, κ a' (f n) :=
by
have h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n := by
rw [h_t1, h_t2, Finset.set_biInter_insert, Set.inter_comm]
filter_upwards [hp_ind (insert a s) h_f_mem] with a' ha'
rw [h_t1_inter_t2, ← ha']
have has : a ∉ s := fun has_mem => haS (hs_mem has_mem)
filter_upwards [h_μ_t1, h_μ_inter] with a' ha1 ha2
rw [ha2, Finset.prod_insert has, h_t2, mul_comm, ha1]
