ofDual_inf' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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