Completed Trellis formalizations produced by others, collected
here as public links. Listing here is not an endorsement of correctness; each is the work of its
respective author. To have a completed formalization added, get in touch.
An atomic decomposition of one-dimensional metric currents without boundary You-Wei Benson Chen, Jesse Goodman, Felipe Hernandez, Daniel Spector