fold_sup_univ — Mathlib

English

In any finite type with SemilatticeSup and a top, the supremum (join) over all elements equals the top.

Русский

В конечном типе, имеющем объединение (верхнюю границу) и максимум, супремум по всем элементам равен верхушке.

LaTeX

$$$\\bigvee_{x \\in \\mathrm{univ}} x = \\top$$$

Lean4

@[simp]
theorem fold_sup_univ [SemilatticeSup α] [OrderTop α] (a : α) : (Finset.univ.fold max a fun x => x) = ⊤ :=
  @fold_inf_univ αᵒᵈ _ _ _ _

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