Surface hypotheses and boundary interface

This file records the manifold assumptions used by the Lean Eval target.

class LeanEval.Topology.ClassificationOfSurfaces.ChartBoundaryInvariant (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : Prop

Topological invariance of the boundary stratum for C0 half-space charts: a mathlib manifold-boundary point is sent by every preferred half-space chart containing it to the frontier of that chart's extended target.

The unconditional C0 instance is proved in Moise/BoundaryInvariant.lean; the interface remains here so low-level surface declarations do not import the invariance-of-domain development.

• chartAt_extend_mem_frontier_target_of_boundary (x : S) {y : S} : y ∈ (chartAt (EuclideanHalfSpace 2) x).source → y ∈ ModelWithCorners.boundary S → ↑((chartAt (EuclideanHalfSpace 2) x).extend (modelWithCornersEuclideanHalfSpace 2)) y ∈ frontier ((chartAt (EuclideanHalfSpace 2) x).extend (modelWithCornersEuclideanHalfSpace 2)).target

instance LeanEval.Topology.ClassificationOfSurfaces.chartBoundaryInvariant_of_contMDiff (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 1 S] : ChartBoundaryInvariant S

structure LeanEval.Topology.ClassificationOfSurfaces.EvalSurface (S : Type u_1) [TopologicalSpace S] : Type u_1

The topological hypotheses in the Lean Eval statement.

Most theorem statements should keep using the typeclass hypotheses directly. This wrapper is useful for blueprint references and for APIs that want to pass the full Eval-surface bundle as data.

• t2 : T2Space S
• connected : ConnectedSpace S
• compact : CompactSpace S
• charted : ChartedSpace (EuclideanHalfSpace 2) S

  The charted declaration.

• manifold : IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S

def LeanEval.Topology.ClassificationOfSurfaces.evalSurface (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : EvalSurface S

Package the active typeclass hypotheses as an EvalSurface.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.evalSurface S = { t2 := ⋯, connected := ⋯, compact := ⋯, charted := inferInstance, manifold := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.eval_surface_hypotheses (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty (EvalSurface S)

Marker theorem packaging the active Eval assumptions.