fold_sup_bot_singleton — Mathlib

English

Let s be a finite set. The supremum (union) of the singleton sets {a} for a in s, starting from the bottom, yields s.

Русский

Пусть s — конечное множество. Объединение (супремум) одноэлементных множеств {a} по a ∈ s начиная с нуля даёт s.

LaTeX

$$$$ \\bigcup_{a \\in s} \\{a\\} = s. $$$$

Lean4

theorem fold_sup_bot_singleton [DecidableEq α] (s : Finset α) : Finset.fold (· ⊔ ·) ⊥ singleton s = s :=
  fold_union_empty_singleton s

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