RightOrdContinuous.orderDual
theorem RightOrdContinuous.orderDual :
∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
This theorem states that for any two types `α` and `β` that both have a preorder, and any function `f` from `α` to `β`, if `f` is right order continuous (meaning it preserves all infima), then the function that applies `f` and then the dual order to its input is left order continuous (meaning it preserves all suprema). This means that reflecting the order of the inputs and the outputs switches the property of preserving the infimum (greatest lower bound) to preserving the supremum (least upper bound).
More concisely: For any right order continuous function from a preordered type to another preordered type, the functional composition with the dual order is left order continuous.
|
LeftOrdContinuous.map_sSup'
theorem LeftOrdContinuous.map_sSup' :
∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
LeftOrdContinuous f → ∀ (s : Set α), f (sSup s) = sSup (f '' s)
The theorem `LeftOrdContinuous.map_sSup'` states that for all types `α` and `β` which form complete lattices, and for any function `f` from `α` to `β` that is left order continuous (meaning it preserves all suprema), the supremum (greatest element) of the image of a set `s` under `f` is the same as the image of the supremum of `s` under `f`. In mathematical terms, if `f` is a function that preserves order and suprema, then `f` applied to the supremum of a set equals the supremum of the image of the set under `f`, i.e., `f(sup(S)) = sup(f(S))` for any set `S`.
More concisely: For any complete lattice types `α` and `β`, and left order continuous function `f` from `α` to `β`, the image of the supremum of a set `s` under `f` is equal to the supremum of the image of `s` under `f`, i.e., `sup(f(s)) = f(sup(s))`.
|