Identity strong-condensation witnesses #
At every seed the ideal conditional law is the original source. The actual joint law agrees exactly, including the zero-division convention for an empty seed alphabet.
theorem
Algebraic.Cutwidth.Extractor.Internal.weightedStrongSeededCondenser_id
{X : Type u_1}
{Seed : Type u_2}
[Fintype X]
[Fintype Seed]
{K : ℕ}
{ε : ℝ}
(nonnegative : 0 ≤ ε)
:
WeightedStrongSeededCondenser (fun (x : X) (x_1 : Seed) => x) K K ε