Documentation

LeanPool.ClassificationOfSurfaces.LeanEval.ChallengeDeps

DO NOT EDIT OR MODIFY

This is the problem definition vendored from https://github.com/leanprover/lean-eval with the sparse checkout generated/topological_classification_of_surfaces

The final submitted solution will live at https://github.com/leanprover/lean-eval which is a pristine verbatim clone of leanprover/lean-eval/generated/topological_classification_of_surfaces

Benchmark statements for topological classification of compact connected surfaces with boundary.

The representative surface in each homeomorphism class is obtained by gluing certain arcs in the boundary of the unit disc.

Reference: Jean Gallier & Dianna Xu, A Guide to the Classification Theorem for Compact Surfaces, Definition 6.5, Lemma 6.1, Theorem 6.1. https://www.cis.upenn.edu/~jean/surfclassif-root.pdf

source
@[reducible, inline]
abbrev Complex.ClosedUnitDisc :
Type

The closed unit disc in the complex plane.

Equations
Instances For
    source
    noncomputable def Complex.ClosedUnitDisc.bdyPtOfReal (r : ℝ) :
    ClosedUnitDisc

    The boundary point exp(2πir) on the boundary of the closed unit disc in the complex plane.

    Equations
    Instances For
      source
      inductive LeanEval.Topology.ClassificationOfSurfaces.OrientableRel (p n : ℕ) :
      Complex.ClosedUnitDisc → Complex.ClosedUnitDisc → Prop

      The representative orientable surface homeomorphic to a closed orientable genus p surface with n discs removed, obtained by identifying the boundary of a disc in the pattern a₁b₁a₁⁻¹b₁⁻¹⋯aₚbₚaₚ⁻¹bₚ⁻¹c₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹.

      Instances For
        source
        inductive LeanEval.Topology.ClassificationOfSurfaces.NonOrientableRel (p n : ℕ) :
        Complex.ClosedUnitDisc → Complex.ClosedUnitDisc → Prop

        The representative non-orientable surface homeomorphic to a direct sum of p projective planes with n discs removed, obtained by identifying the boundary of a disc in the pattern a₁a₁⋯aₚaₚc₁h₁c₁⁻¹⋯cₙhₙcₙ⁻¹.

        Instances For