From e83b173f3d75476e7d5a3723db0d839856b34120 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Sun, 25 Oct 2026 10:29:30 +0000 Subject: [PATCH] doc(Computability.Kolmogorov): add Main results entry for depthBetween_add_depth (#949) --- Complexity/Computability/Kolmogorov/Depth.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Complexity/Computability/Kolmogorov/Depth.lean b/Complexity/Computability/Kolmogorov/Depth.lean index a82e6f56ff..1d22bfabd7 100644 --- a/Complexity/Computability/Kolmogorov/Depth.lean +++ b/Complexity/Computability/Kolmogorov/Depth.lean @@ -36,6 +36,8 @@ exactly the time-bounded complexity. The depth between two time bounds `t₁ ≤ (`exists_forall_le_depth_eq_zero`). * `Cslib.Kolmogorov.DescriptionMethod.depthBetween_add`: depths between consecutive time bounds add up. +* `Cslib.Kolmogorov.DescriptionMethod.depthBetween_add_depth`: depth between two bounds plus depth + at the upper bound equals depth at the lower bound. ## References