ofDual_sup' — Mathlib

English

For nonempty s and f: ι → αᵒᵈ, the OfDual of the supremum equals the infimum of the dual-composed function: ofDual (s.sup' H f) = s.inf' H (ofDual ∘ f).

Русский

Для непустого s и функции f: ι → αᵒᵈ, образ sup' через ofDual равен инфимума через композицию withDual: ofDual (s.sup' H f) = s.inf' H (ofDual ∘ f).

LaTeX

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

Lean4

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

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