English
For a finite index set is, the intersection over i ∈ is of sets s i belongs to a filter f if and only if each s i ∈ f for all i ∈ is.
Русский
Для конечного множества индексов is пересечение по i ∈ is множества s i принадлежит фильтру f тогда и только тогда, когда каждый s i принадлежит f для каждого i ∈ is.
LaTeX
$$$(a)\\ (a)\\left( \\bigcap_{i \\in \\mathrm{is}} s_i \\in f \\right) \\iff \\forall i \\in \\mathrm{is}, s_i \\in f.$$$
Lean4
@[simp]
theorem biInter_mem {β : Type v} {s : β → Set α} {is : Set β} (hf : is.Finite) :
(⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f := by
induction is, hf using Set.Finite.induction_on with
| empty => simp
| insert _ _ hs => simp [hs]
