rightOrdContinuous_dual — Mathlib

English

If f is left order continuous, then the dual composition toDual ∘ f ∘ ofDual is right order continuous.

Русский

Если f слева непрерывна, то композиция с двойственностью правого порядка тоже непрерывна.

LaTeX

$$$\text{LeftOrdContinuous}(f) \Rightarrow \text{RightOrdContinuous}(\mathrm{toDual} \circ f \circ \mathrm{ofDual})$$$

Lean4

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

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