English
If S is a nonempty finite index set and all s(n) ∈ C for n ∈ S, then the finite intersection over i ∈ S of s(i) lies in C.
Русский
Если S не пусто и конечно, и все s(n) ∈ C, то \bigcap_{i∈S} s(i) ∈ C.
LaTeX
$$$S\neq\emptyset,\ S\text{ finite},\ \forall n\in S:\ s(n)\in C \Rightarrow \bigcap_{i\in S} s(i)\in C.$$$
Lean4
theorem biInter_mem {ι : Type*} (hC : IsSetRing C) {s : ι → Set α} (S : Finset ι) (hS : S.Nonempty)
(hs : ∀ n ∈ S, s n ∈ C) : ⋂ i ∈ S, s i ∈ C := by
classical
induction hS using Finset.Nonempty.cons_induction with
| singleton => simpa using hs
| cons i S hiS _ h =>
simp_rw [← Finset.mem_coe, Finset.coe_cons, Set.biInter_insert]
simp only [cons_eq_insert, Finset.mem_insert, forall_eq_or_imp] at hs
refine hC.inter_mem hs.1 ?_
exact h (fun n hnS ↦ hs.2 n hnS)
