CompletePartialOrder.lubOfDirected
theorem CompletePartialOrder.lubOfDirected :
∀ {α : Type u_4} [self : CompletePartialOrder α] (d : Set α),
DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB d (sSup d)
The theorem `CompletePartialOrder.lubOfDirected` states that for any type `α` which has a structure of complete partial order, and for any directed set `d` of `α`, the supremum (denoted `sSup d`) of `d` is the least upper bound of `d`. Here, a set `d` is called directed if for any two elements in the set, there is another element in the set that is greater than or equal to both. The least upper bound of a set is an element which is an upper bound of the set and is less than or equal to any other upper bounds.
More concisely: For any complete partial order `α` and directed set `d` in `α`, the supremum `sSup d` is the unique least upper bound of `d`.
|
DirectedOn.isLUB_sSup
theorem DirectedOn.isLUB_sSup :
∀ {α : Type u_2} [inst : CompletePartialOrder α] {d : Set α},
DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB d (sSup d)
The theorem `DirectedOn.isLUB_sSup` states that for any type `α` with a complete partial order, and any directed set `d` of type `α` where the direction is given by the less than or equal to relation, the supremum (`sSup`) of the set `d` is a least upper bound of `d`. This is the least element that is greater than or equal to all elements in `d`, and in a partial order, if it exists, it is unique. It's worth noting that the notion of `DirectedOn` ensures that for any pair of elements in the set, there is another element in the set that is greater than or equal to both.
More concisely: For any complete partial order `α` and directed set `d ⊆ α` with respect to the less-than-or-equal relation, the supremum of `d` is the unique least upper bound of `d`.
|
CompletePartialOrder.scottContinuous
theorem CompletePartialOrder.scottContinuous :
∀ {α : Type u_2} {β : Type u_3} [inst : CompletePartialOrder α] [inst_1 : Preorder β] {f : α → β},
ScottContinuous f ↔
∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB (f '' d) (f (sSup d))
This theorem, called "Scott-continuity in Complete Partial Orders", states that for any types `α` and `β`, where `α` is a complete partial order, `β` is a preorder, and there is a function `f` mapping from `α` to `β`, the function `f` is Scott-continuous if and only if for all nonempty subsets `d` of `α` that have a directed order (where an element is always less than or equal to another), the least upper bound (supremum) of the image of `d` under `f` is the image under `f` of the supremum of `d`. In other words, `f` preserves the order of elements and their least upper bounds in the transformation from `α` to `β`.
More concisely: A function between complete partial orders is Scott-continuous if and only if it preserves the least upper bounds of directed sets.
|