English
For finite α and a family of Finset α indexed by ι, an element a belongs to the intersection over i of f(i) iff a belongs to every f(i).
Русский
Для конечного α и семейства множеств f(i) индексации ι элемент a принадлежит пересечению по i ∈ s тогда и только тогда, когда a принадлежит каждому f(i).
LaTeX
$$$a \\in s\\inf f \\;\\iff\\; \\forall i \\in s,\\ a \\in f(i)$$$
Lean4
theorem mem_inf [DecidableEq α] {s : Finset ι} {f : ι → Finset α} {a : α} : a ∈ s.inf f ↔ ∀ i ∈ s, a ∈ f i := by
induction s using Finset.cons_induction <;> simp [*]