toDual_sup — Mathlib

English

In the dual order, the supremum corresponds to the infimum in the original order: toDual(s.sup f) = s.inf (toDual ∘ f).

Русский

В двойственном порядке верхняя граница соответствует нижней в исходном порядке: toDual(s.sup f) = s.inf (toDual ∘ f).

LaTeX

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

Lean4

@[simp]
theorem toDual_sup [SemilatticeSup α] [OrderBot α] (s : Finset β) (f : β → α) : toDual (s.sup f) = s.inf (toDual ∘ f) :=
  rfl

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