English
If each π(x) is a π-system, then piiUnionInter π S is a π-system for any S. In other words, the intersection-closure property is preserved under the piiUnionInter construction when every component π(x) is closed under finite intersections.
Русский
Если для каждого x множество π(x) является π‑системой, то piiUnionInter π S также образует π‑систему для любого S. То есть свойство замкнутости при пересечении сохраняется.
LaTeX
$$$\mathrm{IsPiSystem}(\piiUnionInter\pi S)$, если $\forall x, \mathrm{IsPiSystem}(\pi x)$$$
Lean4
/-- If `π` is a family of π-systems, then `piiUnionInter π S` is a π-system. -/
theorem isPiSystem_piiUnionInter (π : ι → Set (Set α)) (hpi : ∀ x, IsPiSystem (π x)) (S : Set ι) :
IsPiSystem (piiUnionInter π S) := by
classical
rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
simp_rw [piiUnionInter, Set.mem_setOf_eq]
let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
use p1 ∪ p2, hp_union_ss, g
have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i :=
by
rw [ht1_eq, ht2_eq]
simp_rw [← Set.inf_eq_inter]
ext1 x
simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
grind
refine ⟨fun n hn => ?_, h_inter_eq⟩
simp only [g]
split_ifs with hn1 hn2 h
· refine hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => ?_)
rw [h_inter_eq] at h_nonempty
suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅ from (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
refine Set.iInter_subset_of_subset hn ?_
grind
· simp [hf1m n hn1]
· simp [hf2m n h]
· exact absurd hn (by simp [hn1, h])
