biInter_finset_mem — Mathlib

English

For a Finset is, the intersection over i ∈ is of sets s i belongs to f iff every s i ∈ f for i ∈ is.

Русский

Для конечного множества индексов is пересечение по i ∈ is множеств s_i принадлежит f тогда и только тогда, когда каждое s_i принадлежит f для каждого i ∈ is.

LaTeX

$$$(\\bigcap_{i \\in \\text{is}} s_i) \\in f \\iff \\forall i \\in \\text{is},\\ s_i \\in f$$$

Lean4

@[simp]
theorem biInter_finset_mem {β : Type v} {s : β → Set α} (is : Finset β) : (⋂ i ∈ is, s i) ∈ f ↔ ∀ i ∈ is, s i ∈ f :=
  biInter_mem is.finite_toSet

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