ofDual_sup — Mathlib

English

For f : β → OrderDual α, the supremum in the dual corresponds to the infimum in α via ofDual: ofDual (s.sup f) = s.inf (ofDual ∘ f).

Русский

Для f : β → OrderDual α верхняя граница в двойственно упорядоченном множестве соответствует инфимума в α: ofDual (s.sup f) = s.inf (ofDual ∘ f).

LaTeX

$$$ ofDual (s.\\sup f) = s.\\inf (ofDual \\circ f) $$$

Lean4

@[simp]
theorem ofDual_sup [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → αᵒᵈ) :
    ofDual (s.sup f) = s.inf (ofDual ∘ f) :=
  rfl

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