Concrete countable dependency closures

For a nonzero vector x, this module closes its finite support under all prepared sequences whose fresh code coordinate has entered the closure. The resulting coordinate set is countable, contains the support of x, and has exactly the closure property required by the transfinite character extension.

def Wallace.ConcreteClosure.closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : Set TriangularPreprocess.ContinuumIndex

The least closure obtained in finitely many dependency steps from the support of x.

Equations

• Wallace.ConcreteClosure.closure N hN M x = Wallace.preparedClosure Wallace.TriangularPreprocess.codeIndex (Wallace.ConcreteData.prepared N hN M) x

theorem Wallace.ConcreteClosure.support_subset_closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : ↑x.support ⊆ closure N hN M x

theorem Wallace.ConcreteClosure.closure_countable (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : (closure N hN M x).Countable

theorem Wallace.ConcreteClosure.prepared_support_mem_closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : TriangularPreprocess.ContinuumIndex) (ha : TriangularPreprocess.codeIndex a ∈ closure N hN M x) (n : ℕ) (i : TriangularPreprocess.ContinuumIndex) (hi : i ∈ (ConcreteData.prepared N hN M a n).support) : i ∈ closure N hN M x

The closure contains every coordinate of each relevant prepared sequence.

theorem Wallace.ConcreteClosure.closure_closedUnderPreparedSupports (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : TransfiniteExtension.ClosedUnderPreparedSupports (ConcreteData.transfiniteData N hN M) (closure N hN M x)