toDual_inf' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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