mem_inf — Mathlib

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 [*]

Похожие утверждения