The Gao--Leung problem and counterexamples

Formalization of the paper's counterexamples concerning order and unbounded-order adherences of sublattices and solid sets.

def OrderClosures.GaoLeungProperty (X : Type u) [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] : Prop

The Gao--Leung question, as a predicate on an ambient vector lattice.

Equations

• OrderClosures.GaoLeungProperty X = ∀ (Y : VectorSublattice X), OrderClosures.IsOrderClosed (OrderClosures.uoAdherence ↑Y)

theorem OrderClosures.gao_counterexample (κ : Cardinal.{u}) : ∃ (K : Type u) (x : TopologicalSpace K) (_ : CompactSpace K) (_ : T2Space K), IsOrderComplete C(K, ℝ) ∧ κ ≤ densityCharacter C(K, ℝ) ∧ ∃ (Y : VectorSublattice C(K, ℝ)), IsClosed ↑Y ∧ TopologicalSpace.IsSeparable ↑Y ∧ ∀ (Z : VectorSublattice C(K, ℝ)), Y ≤ Z → IsOrderClosed ↑Z → Z = ⊤

Paper Proposition 2.1: an order-complete C(K) of arbitrarily large density, with a closed separable sublattice whose only order-closed vector-sublattice extension is all of C(K).

theorem OrderClosures.orderAdherence_cardinality_bound {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] (D : Set X) : Cardinal.mk ↑(orderAdherence D) ≤ 2 ^ 2 ^ Cardinal.mk ↑D

Paper Remark rem:gao-cardinality: cardinality of an arbitrary order adherence.

theorem OrderClosures.exists_solid_large_orderAdherence (κ : Cardinal.{u}) : ∃ (X : Type u) (x : AddCommGroup X) (x_1 : Lattice X) (x_2 : IsOrderedAddMonoid X) (x_3 : VectorLattice X) (S : Set X), LatticeOrderedAddCommGroup.IsSolid S ∧ solidGeneratorNumber S = Cardinal.aleph0 ∧ κ ≤ solidGeneratorNumber (orderAdherence S)

Paper Proposition prop:solid-large-order-closure.

def OrderClosures.positiveSubsetSuprema {X : Type u} [AddCommGroup X] [Lattice X] (S : Set X) : Set X

The class of all suprema of subsets of the positive part of S, used in the proof of Proposition prop:cardinalitybound.

Equations

• OrderClosures.positiveSubsetSuprema S = {x : X | ∃ A ⊆ S ∩ Set.Ici 0, IsLUB A x}

def OrderClosures.signedPositiveSubsetSuprema {X : Type u} [AddCommGroup X] [Lattice X] (S : Set X) : Set X

The order-closed envelope used for the cardinality estimate.

Equations

• OrderClosures.signedPositiveSubsetSuprema S = {x : X | x⁺ ∈ OrderClosures.positiveSubsetSuprema S ∧ x⁻ ∈ OrderClosures.positiveSubsetSuprema S}

theorem OrderClosures.positiveSubsetSuprema_isOrderClosed {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {S : Set X} (hS : LatticeOrderedAddCommGroup.IsSolid S) : IsOrderClosed (positiveSubsetSuprema S)

Isolates the order-closedness of positive subset suprema so it can be reused for the signed envelope in signedPositiveSubsetSuprema_isOrderClosed.

theorem OrderClosures.signedPositiveSubsetSuprema_isOrderClosed {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {S : Set X} (hS : LatticeOrderedAddCommGroup.IsSolid S) : IsOrderClosed (signedPositiveSubsetSuprema S)

Unnumbered assertion in the proof of prop:cardinalitybound.

theorem OrderClosures.solid_orderAdherence_cardinality_bound {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] {S : Set X} (hS : LatticeOrderedAddCommGroup.IsSolid S) : Cardinal.mk ↑(orderAdherence S) ≤ 2 ^ Cardinal.mk ↑S

Paper Proposition prop:cardinalitybound.