A condenser output as a one-block source

The equivalence between an output value and its one-coordinate tuple preserves each point mass. Applying it to the actual output and every conditional witness retains the original statistical distance bound.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_singleton {X : Type u_1} {Earlier : Type u_2} {α : Type u_3} [Fintype X] [Fintype Earlier] [Fintype α] {C : X → Earlier → α} {Kin Kout : ℕ} {ε : ℝ} (cond : WeightedStrongSeededCondenser C Kin Kout ε) (p : X → ℝ) (probability : IsProbabilityWeight p) (cap : CappedWeight p Kin) : ∃ (q : Earlier → (Fin 1 → α) → ℝ), (∀ (y : Earlier), IsBlockSource (q y) Kout) ∧ weightDist (weightedSeededOutput p fun (x : X) (y : Earlier) (x_1 : Fin 1) => C x y) (seedFamilyWeight q) ≤ ε