Countable dependency closures for the rational direct sum

Starting from the finite support of a vector, close under the supports of every prepared sequence whose code coordinate has entered the set.

def Wallace.RationalClosure.closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : Set RationalTriangularPreprocess.ContinuumIndex

Least finite-stage dependency closure of the support of x.

Equations

• Wallace.RationalClosure.closure N hN M x = Wallace.preparedClosure Wallace.RationalTriangularPreprocess.codeIndex (Wallace.RationalData.prepared N hN M) x

theorem Wallace.RationalClosure.support_subset_closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : ↑x.support ⊆ closure N hN M x

theorem Wallace.RationalClosure.closure_countable (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : (closure N hN M x).Countable

theorem Wallace.RationalClosure.prepared_support_mem_closure (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) (a : RationalTriangularPreprocess.ContinuumIndex) (ha : RationalTriangularPreprocess.codeIndex a ∈ closure N hN M x) (n : ℕ) (i : RationalTriangularPreprocess.ContinuumIndex) (hi : i ∈ (RationalData.prepared N hN M a n).support) : i ∈ closure N hN M x

theorem Wallace.RationalClosure.closure_closedUnderPreparedSupports (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : RationalTriangularPreprocess.ContinuumRationalGroup) : RationalTransfiniteExtension.ClosedUnderPreparedSupports (RationalData.transfiniteData N hN M) (closure N hN M x)