toDual_inf — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toDual_inf [SemilatticeInf α] [OrderTop α] (s : Finset β) (f : β → α) : toDual (s.inf f) = s.sup (toDual ∘ f) :=
  rfl

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