fold_inf_univ — Mathlib

English

In any finite type with a SemilatticeInf structure and a bottom, the infimum over all elements equals the bottom element.

Русский

В конечном типе, имеющем полуполу-образную структуру с минимальным элементом, инфимум по всем элементам равен нижнему элементу.

LaTeX

$$$\\bigwedge_{x \\in \\mathrm{univ}} x = \\bot$$$

Lean4

@[simp]
theorem fold_inf_univ [SemilatticeInf α] [OrderBot α] (a : α) : (Finset.univ.fold min a fun x => x) = ⊥ :=
  eq_bot_iff.2 <| ((Finset.fold_op_rel_iff_and <| @le_inf_iff α _).1 le_rfl).2 ⊥ <| Finset.mem_univ _

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