sup_set_eq_biUnion — Mathlib

English

Let s be a finite set of indices and f assigns to each index x ∈ s a subset of some universe. Then the supremum (in the lattice of subsets) of the family {f(x) : x ∈ s} equals the union of these sets. In symbols: s.sup f = ⋃_{x ∈ s} f(x).

Русский

Пусть s — конечное множество индексов, и каждому x ∈ s поставлено подмножество f(x). Тогда супремум семейства {f(x) : x ∈ s} в решетке подмножеств равен их объединению: s.sup f = ⋃_{x ∈ s} f(x).

LaTeX

$$$ s \sup f = \bigcup_{x \in s} f(x) $$$

Lean4

@[simp]
theorem sup_set_eq_biUnion (s : Finset α) (f : α → Set β) : s.sup f = ⋃ x ∈ s, f x :=
  sup_eq_iSup _ _

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