ofDual_sSup — Mathlib

English

The infimum of the dual supremum corresponds to the supremum of the dual preimage.

Русский

Убывающую верхнюю границу двойственно отображаемого множества соответствуют верхние границы двойственного образа.

LaTeX

$$$\operatorname{ofDual}(\sSup s) = \sInf (\operatorname{toDual}^{-1} s)$$$

Lean4

@[simp]
theorem ofDual_sSup [InfSet α] (s : Set αᵒᵈ) : ofDual (sSup s) = sInf (toDual ⁻¹' s) :=
  rfl

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