definition order_converge ≝
λO:ordered_set.λa:sequence O.λx:O.
exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
- (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
+ (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
(u i) is_supremum ⌊w,a (w+i)⌋).
notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45