The Banach lattice Lean library (arxiv.org)

We present a Lean 4 library for the theory of Banach lattices. Its purpose is to support the systematic formalization of contemporary research in Banach lattices and related areas. As evidence of this...