Directed Topology Lean 4

Lawson, Dominique

doi:10.4230/artifacts.22493

Artifact

Directed Topology Lean 4 Software

Author Dominique Lawson

Part of: Collection: Supplementary Materials
License: MIT License
Publication Date: 2024-11-28

Document Identifiers

DOI: 10.4230/artifacts.22493
URN: urn:nbn:de:0030-drops-224931

Author Details

Dominique Lawson

Leiden University, The Netherlands

Content

Software (Lean Code): https://github.com/Dominique-Lawson/Directed-Topology-Lean-4
archived version

Version/Status

Content created at: 2023-10-17
Status: Active (at the time of publication 2024-11-28)

Cite As Get BibTex

Dominique Lawson. Directed Topology Lean 4 (Software, Lean Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/artifacts.22493

Description

The repository contains a formalisation of the field of directed topology with the aim of proving the Van Kampen Theorem for directed spaces in Lean 4.

Subject Classification

Keywords

Lean
Directed Topology
Van Kampen Theorem
Formalisation

Programming Languages

Lean

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Metadata Views

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail