inf_set_eq_iInter — Mathlib

English

Let s be a finite index set and f: α → Set β. Then the infimum of the family {f(x)}_{x∈s} equals the intersection of all f(x) for x in s.

Русский

Пусть s — конечное множество индексов и f: α → Set β. Тогда инфимум семейства множеств {f(x)} по x∈s равен пересечению всех множеств f(x).

LaTeX

$$$\inf_{x \in s} f(x) = \bigcap_{x \in s} f(x)$$$

Lean4

@[simp]
theorem inf_set_eq_iInter (s : Finset α) (f : α → Set β) : s.inf f = ⋂ x ∈ s, f x :=
  inf_eq_iInf _ _

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