The Cantor–Bendixson convex cover has a nondegenerate model

The partition hypotheses require a nested well-ordered neighborhood base at zero consisting of open convex subgroups. The real line does not satisfy them: its only convex subgroups are zero and the whole line, and zero is not open. Any witness is therefore non-Archimedean, and this file supplies one: real sequences indexed by the naturals under the lexicographic order, with the subgroups of sequences vanishing below a given index.

Those subgroups are nested, convex, open, and coinitial, so the hypotheses are consistent and the geometric part of the cofactor construction is not vacuous. The check also separates the openness requirement from the trivial family: the zero subgroup alone satisfies every other condition.

@[reducible, inline]

abbrev Tests.CantorBendixsonConvexCover.LexSeq : Type

Real sequences under the lexicographic order: a non-Archimedean ordered abelian group.

Equations

• Tests.CantorBendixsonConvexCover.LexSeq = Lex (ℕ → ℝ)

@[reducible, inline]

abbrev Tests.CantorBendixsonConvexCover.entry (x : LexSeq) (k : ℕ) : ℝ

The entries of a lexicographic sequence.

Equations

• Tests.CantorBendixsonConvexCover.entry x k = ofLex x k

theorem Tests.CantorBendixsonConvexCover.entry_add (x y : LexSeq) (k : ℕ) : entry (x + y) k = entry x k + entry y k

theorem Tests.CantorBendixsonConvexCover.entry_neg (x : LexSeq) (k : ℕ) : entry (-x) k = -entry x k

theorem Tests.CantorBendixsonConvexCover.entry_zero (k : ℕ) : entry 0 k = 0

theorem Tests.CantorBendixsonConvexCover.entry_sub (x y : LexSeq) (k : ℕ) : entry (x - y) k = entry x k - entry y k

theorem Tests.CantorBendixsonConvexCover.lt_of_forall_eq_of_lt {x y : LexSeq} {m : ℕ} (h : ∀ j < m, entry x j = entry y j) (hm : entry x m < entry y m) : x < y

@[instance_reducible]

instance Tests.CantorBendixsonConvexCover.instTopologicalSpaceLexSeq : TopologicalSpace LexSeq

Equations

• Tests.CantorBendixsonConvexCover.instTopologicalSpaceLexSeq = Preorder.topology Tests.CantorBendixsonConvexCover.LexSeq

instance Tests.CantorBendixsonConvexCover.instOrderTopologyLexSeq : OrderTopology LexSeq

def Tests.CantorBendixsonConvexCover.vanishingBelow (n : ℕ) : AddSubgroup LexSeq

The subgroup of sequences vanishing below a given index.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Tests.CantorBendixsonConvexCover.mem_vanishingBelow {n : ℕ} {x : LexSeq} : x ∈ vanishingBelow n ↔ ∀ k < n, entry x k = 0

theorem Tests.CantorBendixsonConvexCover.vanishingBelow_mono {i j : ℕ} (hij : i ≤ j) : ↑(vanishingBelow j) ⊆ ↑(vanishingBelow i)

The witnessing family is nested and decreasing.

theorem Tests.CantorBendixsonConvexCover.exists_least_ne_zero {c : LexSeq} {k : ℕ} (hne : entry c k ≠ 0) : ∃ (m : ℕ), entry c m ≠ 0 ∧ ∀ j < m, entry c j = 0

The least index at which a nonzero sequence does not vanish.

theorem Tests.CantorBendixsonConvexCover.vanishingBelow_ordConnected (n : ℕ) : (↑(vanishingBelow n)).OrdConnected

Each subgroup of the family is convex: a sequence between two vanishing ones has no earlier nonzero entry, since a positive one would exceed the upper bound and a negative one would fall below the lower bound.

def Tests.CantorBendixsonConvexCover.unitAt (n : ℕ) : LexSeq

The indicator sequence with a single unit entry.

Equations

• Tests.CantorBendixsonConvexCover.unitAt n = toLex fun (k : ℕ) => if k = n then 1 else 0

theorem Tests.CantorBendixsonConvexCover.entry_unitAt (n k : ℕ) : entry (unitAt n) k = if k = n then 1 else 0

theorem Tests.CantorBendixsonConvexCover.unitAt_pos (n : ℕ) : 0 < unitAt n

theorem Tests.CantorBendixsonConvexCover.vanishingBelow_subset_Ioo (n : ℕ) : ↑(vanishingBelow (n + 1)) ⊆ Set.Ioo (-unitAt n) (unitAt n)

Every sequence vanishing below an index lies strictly between the negative and positive unit sequences at that index, so each subgroup of the family contains a neighborhood of zero and is therefore open.

theorem Tests.CantorBendixsonConvexCover.vanishingBelow_isOpen (n : ℕ) : IsOpen ↑(vanishingBelow n)

theorem Tests.CantorBendixsonConvexCover.exists_vanishingBelow_subset_Ioo {ε : LexSeq} (hε : 0 < ε) : ∃ (n : ℕ), ↑(vanishingBelow n) ⊆ Set.Ioo (-ε) ε

The family is coinitial: every strictly positive sequence dominates one of its members.

instance Tests.CantorBendixsonConvexCover.instNoMinOrderLexSeq : NoMinOrder LexSeq

instance Tests.CantorBendixsonConvexCover.instNoMaxOrderLexSeq : NoMaxOrder LexSeq

theorem Tests.CantorBendixsonConvexCover.exists_disjoint_convex_cover_with_rank_lt_center_lexSeq (s : TopologicalSpace.Closeds LexSeq) (hs : (↑s).IsPWO) : ∃ (X : Set LexSeq) (C : ↑X → Set LexSeq), X ⊆ ↑s ∧ (∀ (x : ↑X), ↑x ∈ C x) ∧ (∀ (x : ↑X), IsOpen (C x)) ∧ (∀ (x : ↑X), (C x).OrdConnected) ∧ (∀ (x y : ↑X), x ≠ y → Disjoint (C x) (C y)) ∧ (∀ (x y : ↑X), ↑x < ↑y → ∀ a ∈ C x, ∀ b ∈ C y, a < b) ∧ ↑s ⊆ ⋃ (x : ↑X), C x ∧ (∀ (x : ↑X), ∀ z ∈ ↑s ∩ C x, z ≤ ↑x) ∧ (∀ (x : ↑X), ∀ z ∈ ↑s ∩ C x, z ≠ ↑x → s.cantorBendixsonRank hs z < s.cantorBendixsonRank hs ↑x) ∧ ∀ (z : LexSeq), ¬AccPt z (Filter.principal X)

The cover hypotheses are consistent. Every hypothesis of the disjoint convex cover theorem holds for the lexicographic sequence group with the vanishing-below family, so the result is not vacuous.

theorem Tests.CantorBendixsonConvexCover.not_isOpen_bot_real : ¬IsOpen ↑⊥

The real line is not a witness: its only convex subgroups are zero and the whole line, and zero is not open, so no family of open convex subgroups is a neighborhood base at zero. The openness requirement is therefore doing real work.