iInter_mem — Mathlib

English

For a finite index type β, the intersection over all i of sets s_i belongs to f iff every s_i ∈ f.

Русский

Для конечного множества индексов β пересечение по i всех s_i принадлежит фильтру f тогда и только тогда, когда каждый s_i принадлежит f.

LaTeX

$$$(\\bigcap_{i} s_i) \\in f \\iff ∀ i, s_i \\in f$ (при условии скалярной конечности β).$$

Lean4

@[simp]
theorem iInter_mem {β : Sort v} {s : β → Set α} [Finite β] : (⋂ i, s i) ∈ f ↔ ∀ i, s i ∈ f :=
  (sInter_mem (finite_range _)).trans forall_mem_range

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