Directed Topology Lean 4 Software

Author Dominique Lawson



Document Identifiers

Author Details

Dominique Lawson
  • Leiden University, The Netherlands

Content

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

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail