ofDual_inf — Mathlib

English

Repetition of fold-r inf equality for lists: the same relation as in item 95037.

Русский

Повторение утверждения о равенстве свёртки по правому краю инфимуму и инфимума списка.

LaTeX

$$$ List.foldr (\\\\lambda x_1 x_2 \\\\to x_1 \\\\wedge x_2) \\top l = l.\\\\toFinset.inf id $$$

Lean4

@[simp]
theorem ofDual_inf [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → αᵒᵈ) :
    ofDual (s.inf f) = s.sup (ofDual ∘ f) :=
  rfl

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