toDual_sup' — Mathlib

English

For any nonempty finite s and function f, the supremum under the dual order corresponds to the infimum under dual: toDual (s.sup' H f) = s.inf' H (toDual ∘ f).

Русский

Для любого непустого конечного множества и функции sup' над ним соответствует инфимума под двойственным порядком: toDual (s.sup' H f) = s.inf' H (toDual ∘ f).

LaTeX

$$$\mathrm{toDual}\bigl(s.sup' H f\bigr) = s.inf' H (\mathrm{toDual} \circ f).$$$

Lean4

@[simp]
theorem toDual_sup' [SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) :
    toDual (s.sup' hs f) = s.inf' hs (toDual ∘ f) :=
  rfl

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