Simple arcs in a topological space

Definition

LeanFormalizations_PachDeZeeuw_CrossingLemma_PlaneArcSeparation

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

topology

A simple arc is a continuous injective map from the closed unit interval into a topological space.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/

namespace CrossingLemma.PlaneArcSeparation

open Set Topology


structure SimpleArc (X : Type*) [TopologicalSpace X] where
   
  toFun : Set.Icc (0 : ℝ) 1 → X
   
  continuous_toFun : Continuous toFun
   
  injective_toFun : Function.Injective toFun

attribute [coe] SimpleArc.toFun

instance {X : Type*} [TopologicalSpace X] :
    CoeFun (SimpleArc X) (fun _ => Set.Icc (0 : ℝ) 1 → X) := ⟨SimpleArc.toFun⟩

namespace SimpleArc

variable {X : Type*} [TopologicalSpace X]


end SimpleArc


variable {X : Type*} [TopologicalSpace X]


end CrossingLemma.PlaneArcSeparation

View graph