English
A nonempty finite intersection of sets in a π-system belongs to the π-system.
Русский
Непустое конечное пересечение множест в π–системе принадлежит этой же π–системе.
LaTeX
$$$ (⋂ s ∈ t, s) ∈ S $$$
Lean4
/-- A nonempty finite intersection of sets in a π-system belongs to the π-system. -/
theorem biInter_mem {S : Set (Set α)} (h_pi : IsPiSystem S) {t : Finset (Set α)} (t_ne : t.Nonempty)
(ht : ∀ s ∈ t, s ∈ S) (h' : (⋂ s ∈ t, s).Nonempty) : (⋂ s ∈ t, s) ∈ S := by
classical
induction t_ne using Finset.Nonempty.cons_induction with
| singleton a => simpa using ht
| cons a t hat t_ne
ih =>
simp only [Finset.cons_eq_insert, Finset.mem_insert, iInter_iInter_eq_or_left] at h' ht ⊢
refine h_pi _ (ht a (Or.inl rfl)) _ ?_ h'
refine ih (fun s hs ↦ ?_) h'.right
exact ht s (Or.inr hs)
