English
For a finite index set ι, membership in ⨅ i∈ι f(i) is equivalent to the existence of a family t(i) with t(i) ∈ f(i) for all i, and s = ⋂ i∈ι t(i).
Русский
Для конечного множества индексов ι принадлежность s в ⨅ i∈ι f(i) эквивалентна существованию семейства t(i) такое, что t(i) ∈ f(i) для всех i и s = ⋂ i∈ι t(i).
LaTeX
$$$ s \in \iInf_{i \in ι} f(i) \iff \exists t : Finset ι, s \in \iInf_{i \in t} f(i) $$
Lean4
theorem mem_iInf_of_finite {ι : Sort*} [Finite ι] {α : Type*} {f : ι → Filter α} (s) :
(s ∈ ⨅ i, f i) ↔ ∃ t : ι → Set α, (∀ i, t i ∈ f i) ∧ s = ⋂ i, t i :=
by
refine ⟨exists_iInter_of_mem_iInf, ?_⟩
rintro ⟨t, ht, rfl⟩
exact iInter_mem.2 fun i => mem_iInf_of_mem i (ht i)
