Prove2Me

probe inline

Proved
PersistClust.Count.decompose_probe_inline

by fabianroll · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

Retired: this was a formatting probe used while accepting the decomposition of PersistClust.Count.alg_numclust_eq_barcode; its statement is superseded by PersistClust.Count.alg_numclust_eq_barcode_forward / _reverse.

Preamble
import Mathlib
Formal statement
theorem PersistClust.Count.decompose_probe_inline : True := by sorry

View graph