English
If each C(i) is a Pi-system and univ ∈ C(i) for all i, then squareCylinders(C) forms a Pi-system.
Русский
Если для каждого i C(i) является пи-системой и единица принадлежит каждой C(i), то squareCylinders(C) образует пи-систему.
LaTeX
$$$$\\text{IsPiSystem}(\\text{squareCylinders}(C))$$ under hypotheses $\\forall i, \\text{IsPiSystem}(C(i))$ and $\\forall i, \\text{univ} \\in C(i)$.$$
Lean4
theorem isPiSystem_squareCylinders {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) (hC_univ : ∀ i, univ ∈ C i) :
IsPiSystem (squareCylinders C) :=
by
rintro S₁ ⟨s₁, t₁, h₁, rfl⟩ S₂ ⟨s₂, t₂, h₂, rfl⟩ hst_nonempty
classical
let t₁' := s₁.piecewise t₁ (fun i ↦ univ)
let t₂' := s₂.piecewise t₂ (fun i ↦ univ)
have h1 : ∀ i ∈ (s₁ : Set ι), t₁ i = t₁' i := fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
have h1' : ∀ i ∉ (s₁ : Set ι), t₁' i = univ := fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
have h2 : ∀ i ∈ (s₂ : Set ι), t₂ i = t₂' i := fun i hi ↦ (Finset.piecewise_eq_of_mem _ _ _ hi).symm
have h2' : ∀ i ∉ (s₂ : Set ι), t₂' i = univ := fun i hi ↦ Finset.piecewise_eq_of_notMem _ _ _ hi
rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, ← union_pi_inter h1' h2']
refine ⟨s₁ ∪ s₂, fun i ↦ t₁' i ∩ t₂' i, ?_, ?_⟩
· rw [mem_univ_pi]
intro i
have : (t₁' i ∩ t₂' i).Nonempty := by
obtain ⟨f, hf⟩ := hst_nonempty
rw [Set.pi_congr rfl h1, Set.pi_congr rfl h2, mem_inter_iff, mem_pi, mem_pi] at hf
refine ⟨f i, ⟨?_, ?_⟩⟩
· by_cases hi₁ : i ∈ s₁
· exact hf.1 i hi₁
· rw [h1' i hi₁]
exact mem_univ _
· by_cases hi₂ : i ∈ s₂
· exact hf.2 i hi₂
· rw [h2' i hi₂]
exact mem_univ _
refine hC i _ ?_ _ ?_ this
· by_cases hi₁ : i ∈ s₁
· rw [← h1 i hi₁]
exact h₁ i (mem_univ _)
· rw [h1' i hi₁]
exact hC_univ i
· by_cases hi₂ : i ∈ s₂
· rw [← h2 i hi₂]
exact h₂ i (mem_univ _)
· rw [h2' i hi₂]
exact hC_univ i
· rw [Finset.coe_union]
