The Gao--Leung order-continuity characterization

This file proves Gao--Leung Theorem 2.7. The reverse implication is obtained by contrapositive: failure of order continuity supplies an order-bounded disjoint sequence, which gives a lattice embedding of ℓ∞(ℕ × ℕ) into the ambient Banach lattice. The row-limit sublattice then separates uo-adherence from order adherence.

theorem OrderClosures.gaoLeung_orderContinuous_characterization {X : Type u} [NormedAddCommGroup X] [SigmaConditionallyCompleteLattice X] [IsOrderedAddMonoid X] [BanachLattice X] : ((∀ (Y : VectorSublattice X), IsOrderClosed (orderAdherence ↑Y)) ↔ ∀ (Y : VectorSublattice X), orderAdherence ↑Y = uoAdherence ↑Y) ∧ ((∀ (Y : VectorSublattice X), orderAdherence ↑Y = uoAdherence ↑Y) ↔ IsOrderContinuousNorm X)

Gao--Leung, Theorem 2.7 (paper Theorem ND).