Directed Topology in Lean 4

Source: arxiv:2312.06506, doi:10.4230/LIPIcs.ITP.2024.8 Authors: Dominique Lawson, Henning Basold, Peter Bruin Status: verified Main declarations: DirectedSpace, Dipath, DirectedVanKampen.directed_van_kampen Tags: directed-topology, algebraic-topology, category-theory MSC: 55U40, 55Q05, 18A30