orderDual — Mathlib

English

If f: α → β is RightOrdContinuous, then the dual-conjugate function f* := toDual ∘ f ∘ ofDual: α^op → β^op is LeftOrdContinuous.

Русский

Если f: α → β является правой непрерывной, то функция f*, полученная через двойственность порядка, является левой непрерывной.

LaTeX

$$$ \\text{LeftOrdContinuous}(f^*) \\text{ where } f^* = \\mathrm{toDual} \\circ f \\circ \\mathrm{ofDual}. $$$

Lean4

protected theorem orderDual : RightOrdContinuous f → LeftOrdContinuous (toDual ∘ f ∘ ofDual) :=
  id

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