Documentation

Mathlib.Topology.Connected.PathConnected

Path connectedness #

Main definitions #

In the file the unit interval [0, 1] in is denoted by I, and X is a topological space.

Then there are corresponding relative notions for F : Set X.

## Main theorems

One can link the absolute and relative version in two directions, using (univ : Set X) or the subtype ↥F.

For locally path connected spaces, we have

Implementation notes #

By default, all paths have I as their source and X as their target, but there is an operation Set.IccExtend that will extend any continuous map γ : I → X into a continuous map IccExtend zero_le_one γ : ℝ → X that is constant before 0 and after 1.

This is used to define Path.extend that turns γ : Path x y into a continuous map γ.extend : ℝ → X whose restriction to I is the original γ, and is equal to x on (-∞, 0] and to y on [1, +∞).

Paths #

structure Path {X : Type u_1} [TopologicalSpace X] (x : X) (y : X) extends ContinuousMap :
Type u_1

Continuous path connecting two points x and y in a topological space

  • toFun : unitIntervalX
  • continuous_toFun : Continuous self.toFun
  • source' : self.toFun 0 = x

    The start point of a Path.

  • target' : self.toFun 1 = y

    The end point of a Path.

Instances For
    theorem Path.source' {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (self : Path x y) :
    self.toFun 0 = x

    The start point of a Path.

    theorem Path.target' {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (self : Path x y) :
    self.toFun 1 = y

    The end point of a Path.

    instance Path.funLike {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
    Equations
    • Path.funLike = { coe := fun (γ : Path x y) => γ.toContinuousMap, coe_injective' := }
    instance Path.continuousMapClass {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
    Equations
    • =
    theorem Path.ext {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {γ₁ : Path x y} {γ₂ : Path x y} :
    γ₁ = γ₂γ₁ = γ₂
    @[simp]
    theorem Path.coe_mk_mk {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (f : unitIntervalX) (h₁ : Continuous f) (h₂ : f 0 = x) (h₃ : f 1 = y) :
    { toFun := f, continuous_toFun := h₁, source' := h₂, target' := h₃ } = f
    theorem Path.continuous {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
    @[simp]
    theorem Path.source {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
    γ 0 = x
    @[simp]
    theorem Path.target {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
    γ 1 = y
    def Path.simps.apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
    unitIntervalX

    See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.

    Equations
    Instances For
      @[simp]
      theorem Path.coe_toContinuousMap {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
      γ.toContinuousMap = γ
      @[simp]
      theorem Path.coe_mk {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
      γ = γ
      instance Path.hasUncurryPath {X : Type u_4} {α : Type u_5} [TopologicalSpace X] {x : αX} {y : αX} :
      Function.HasUncurry ((a : α) → Path (x a) (y a)) (α × unitInterval) X

      Any function φ : Π (a : α), Path (x a) (y a) can be seen as a function α × I → X.

      Equations
      • Path.hasUncurryPath = { uncurry := fun (φ : (a : α) → Path (x a) (y a)) (p : α × unitInterval) => (φ p.1) p.2 }
      @[simp]
      theorem Path.refl_apply {X : Type u_1} [TopologicalSpace X] (x : X) (_t : unitInterval) :
      (Path.refl x) _t = x
      def Path.refl {X : Type u_1} [TopologicalSpace X] (x : X) :
      Path x x

      The constant path from a point to itself

      Equations
      • Path.refl x = { toFun := fun (_t : unitInterval) => x, continuous_toFun := , source' := , target' := }
      Instances For
        @[simp]
        theorem Path.refl_range {X : Type u_1} [TopologicalSpace X] {a : X} :
        Set.range (Path.refl a) = {a}
        @[simp]
        theorem Path.symm_apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
        ∀ (a : unitInterval), γ.symm a = (γ unitInterval.symm) a
        def Path.symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
        Path y x

        The reverse of a path from x to y, as a path from y to x

        Equations
        • γ.symm = { toFun := γ unitInterval.symm, continuous_toFun := , source' := , target' := }
        Instances For
          @[simp]
          theorem Path.symm_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
          γ.symm.symm = γ
          theorem Path.symm_bijective {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
          @[simp]
          theorem Path.refl_symm {X : Type u_1} [TopologicalSpace X] {a : X} :
          (Path.refl a).symm = Path.refl a
          @[simp]
          theorem Path.symm_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
          Set.range γ.symm = Set.range γ

          Space of paths #

          instance Path.topologicalSpace {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :

          The following instance defines the topology on the path space to be induced from the compact-open topology on the space C(I,X) of continuous maps from I to X.

          Equations
          theorem Path.continuous_eval {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
          Continuous fun (p : Path x y × unitInterval) => p.1 p.2
          theorem Continuous.path_eval {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {Y : Type u_4} [TopologicalSpace Y] {f : YPath x y} {g : YunitInterval} (hf : Continuous f) (hg : Continuous g) :
          Continuous fun (y_1 : Y) => (f y_1) (g y_1)
          theorem Path.continuous_uncurry_iff {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {Y : Type u_4} [TopologicalSpace Y] {g : YPath x y} :
          def Path.extend {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
          X

          A continuous map extending a path to , constant before 0 and after 1.

          Equations
          Instances For
            theorem Continuous.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {γ : YPath x y} {f : Y} (hγ : Continuous γ) (hf : Continuous f) :
            Continuous fun (t : Y) => (γ t).extend (f t)

            See Note [continuity lemma statement].

            theorem Path.continuous_extend {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
            Continuous γ.extend

            A useful special case of Continuous.path_extend.

            theorem Filter.Tendsto.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {l : YX} {r : YX} {y : Y} {l₁ : Filter } {l₂ : Filter X} {γ : (y : Y) → Path (l y) (r y)} (hγ : Filter.Tendsto (γ) (nhds y ×ˢ Filter.map (Set.projIcc 0 1 ) l₁) l₂) :
            Filter.Tendsto (fun (x : Y) => (γ x).extend) (nhds y ×ˢ l₁) l₂
            theorem ContinuousAt.path_extend {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {g : Y} {l : YX} {r : YX} (γ : (y : Y) → Path (l y) (r y)) {y : Y} (hγ : ContinuousAt (γ) (y, Set.projIcc 0 1 (g y))) (hg : ContinuousAt g y) :
            ContinuousAt (fun (i : Y) => (γ i).extend (g i)) y
            @[simp]
            theorem Path.extend_extends {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : } (ht : t Set.Icc 0 1) :
            γ.extend t = γ t, ht
            theorem Path.extend_zero {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
            γ.extend 0 = x
            theorem Path.extend_one {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
            γ.extend 1 = y
            @[simp]
            theorem Path.extend_extends' {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : (Set.Icc 0 1)) :
            γ.extend t = γ t
            @[simp]
            theorem Path.extend_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
            Set.range γ.extend = Set.range γ
            theorem Path.extend_of_le_zero {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : } (ht : t 0) :
            γ.extend t = a
            theorem Path.extend_of_one_le {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t : } (ht : 1 t) :
            γ.extend t = b
            @[simp]
            theorem Path.refl_extend {X : Type u_1} [TopologicalSpace X] {a : X} :
            (Path.refl a).extend = fun (x : ) => a
            def Path.ofLine {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {f : X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) :
            Path x y

            The path obtained from a map defined on by restriction to the unit interval.

            Equations
            • Path.ofLine hf h₀ h₁ = { toFun := f Subtype.val, continuous_toFun := , source' := h₀, target' := h₁ }
            Instances For
              theorem Path.ofLine_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {f : X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) (t : unitInterval) :
              (Path.ofLine hf h₀ h₁) t f '' unitInterval
              def Path.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) :
              Path x z

              Concatenation of two paths from x to y and from y to z, putting the first path on [0, 1/2] and the second one on [1/2, 1].

              Equations
              • γ.trans γ' = { toFun := (fun (t : ) => if t 1 / 2 then γ.extend (2 * t) else γ'.extend (2 * t - 1)) Subtype.val, continuous_toFun := , source' := , target' := }
              Instances For
                theorem Path.trans_apply {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) (t : unitInterval) :
                (γ.trans γ') t = if h : t 1 / 2 then γ 2 * t, else γ' 2 * t - 1,
                @[simp]
                theorem Path.trans_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) :
                (γ.trans γ').symm = γ'.symm.trans γ.symm
                @[simp]
                theorem Path.refl_trans_refl {X : Type u_1} [TopologicalSpace X] {a : X} :
                (Path.refl a).trans (Path.refl a) = Path.refl a
                theorem Path.trans_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} {c : X} (γ₁ : Path a b) (γ₂ : Path b c) :
                Set.range (γ₁.trans γ₂) = Set.range γ₁ Set.range γ₂
                def Path.map' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : XY} (h : ContinuousOn f (Set.range γ)) :
                Path (f x) (f y)

                Image of a path from x to y by a map which is continuous on the path.

                Equations
                • γ.map' h = { toFun := f γ, continuous_toFun := , source' := , target' := }
                Instances For
                  def Path.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : XY} (h : Continuous f) :
                  Path (f x) (f y)

                  Image of a path from x to y by a continuous map

                  Equations
                  • γ.map h = γ.map'
                  Instances For
                    @[simp]
                    theorem Path.map_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : XY} (h : Continuous f) :
                    (γ.map h) = f γ
                    @[simp]
                    theorem Path.map_symm {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {f : XY} (h : Continuous f) :
                    (γ.map h).symm = γ.symm.map h
                    @[simp]
                    theorem Path.map_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {z : X} (γ : Path x y) (γ' : Path y z) {f : XY} (h : Continuous f) :
                    (γ.trans γ').map h = (γ.map h).trans (γ'.map h)
                    @[simp]
                    theorem Path.map_id {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
                    γ.map = γ
                    @[simp]
                    theorem Path.map_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} (γ : Path x y) {Z : Type u_4} [TopologicalSpace Z] {f : XY} (hf : Continuous f) {g : YZ} (hg : Continuous g) :
                    (γ.map hf).map hg = γ.map
                    def Path.cast {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {x' : X} {y' : X} (hx : x' = x) (hy : y' = y) :
                    Path x' y'

                    Casting a path from x to y to a path from x' to y' when x' = x and y' = y

                    Equations
                    • γ.cast hx hy = { toFun := γ, continuous_toFun := , source' := , target' := }
                    Instances For
                      @[simp]
                      theorem Path.symm_cast {X : Type u_1} [TopologicalSpace X] {a₁ : X} {a₂ : X} {b₁ : X} {b₂ : X} (γ : Path a₂ b₂) (ha : a₁ = a₂) (hb : b₁ = b₂) :
                      (γ.cast ha hb).symm = γ.symm.cast hb ha
                      @[simp]
                      theorem Path.trans_cast {X : Type u_1} [TopologicalSpace X] {a₁ : X} {a₂ : X} {b₁ : X} {b₂ : X} {c₁ : X} {c₂ : X} (γ : Path a₂ b₂) (γ' : Path b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂) (hc : c₁ = c₂) :
                      (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc
                      @[simp]
                      theorem Path.cast_coe {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {x' : X} {y' : X} (hx : x' = x) (hy : y' = y) :
                      (γ.cast hx hy) = γ
                      theorem Path.symm_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ιX} {b : ιX} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous γ) :
                      Continuous fun (t : ι) => (γ t).symm
                      theorem Path.continuous_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
                      Continuous Path.symm
                      theorem Path.continuous_uncurry_extend_of_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ιX} {b : ιX} (γ : (t : ι) → Path (a t) (b t)) (h : Continuous γ) :
                      Continuous fun (t : ι) => (γ t).extend
                      theorem Path.trans_continuous_family {X : Type u_1} [TopologicalSpace X] {ι : Type u_4} [TopologicalSpace ι] {a : ιX} {b : ιX} {c : ιX} (γ₁ : (t : ι) → Path (a t) (b t)) (h₁ : Continuous γ₁) (γ₂ : (t : ι) → Path (b t) (c t)) (h₂ : Continuous γ₂) :
                      Continuous fun (t : ι) => (γ₁ t).trans (γ₂ t)
                      theorem Continuous.path_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : X} {z : X} {f : YPath x y} {g : YPath y z} :
                      Continuous fContinuous gContinuous fun (t : Y) => (f t).trans (g t)
                      theorem Path.continuous_trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} :
                      Continuous fun (ρ : Path x y × Path y z) => ρ.1.trans ρ.2

                      Product of paths #

                      def Path.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {b₁ : Y} {b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) :
                      Path (a₁, b₁) (a₂, b₂)

                      Given a path in X and a path in Y, we can take their pointwise product to get a path in X × Y.

                      Equations
                      • γ₁.prod γ₂ = { toContinuousMap := γ₁.prodMk γ₂.toContinuousMap, source' := , target' := }
                      Instances For
                        @[simp]
                        theorem Path.prod_coe {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {b₁ : Y} {b₂ : Y} (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) :
                        (γ₁.prod γ₂) = fun (t : unitInterval) => (γ₁ t, γ₂ t)
                        theorem Path.trans_prod_eq_prod_trans {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {a₁ : X} {a₂ : X} {a₃ : X} {b₁ : Y} {b₂ : Y} {b₃ : Y} (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂) (δ₂ : Path b₂ b₃) :
                        (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)

                        Path composition commutes with products

                        def Path.pi {ι : Type u_3} {χ : ιType u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) :
                        Path as bs

                        Given a family of paths, one in each Xᵢ, we take their pointwise product to get a path in Π i, Xᵢ.

                        Equations
                        • Path.pi γ = { toContinuousMap := ContinuousMap.pi fun (i : ι) => (γ i).toContinuousMap, source' := , target' := }
                        Instances For
                          @[simp]
                          theorem Path.pi_coe {ι : Type u_3} {χ : ιType u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} (γ : (i : ι) → Path (as i) (bs i)) :
                          (Path.pi γ) = fun (t : unitInterval) (i : ι) => (γ i) t
                          theorem Path.trans_pi_eq_pi_trans {ι : Type u_3} {χ : ιType u_4} [(i : ι) → TopologicalSpace (χ i)] {as : (i : ι) → χ i} {bs : (i : ι) → χ i} {cs : (i : ι) → χ i} (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (bs i) (cs i)) :
                          (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun (i : ι) => (γ₀ i).trans (γ₁ i)

                          Path composition commutes with products

                          Pointwise multiplication/addition of two paths in a topological (additive) group #

                          def Path.add {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) :
                          Path (a₁ + a₂) (b₁ + b₂)

                          Pointwise addition of paths in a topological additive group.

                          Equations
                          • γ₁.add γ₂ = (γ₁.prod γ₂).map
                          Instances For
                            def Path.mul {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) :
                            Path (a₁ * a₂) (b₁ * b₂)

                            Pointwise multiplication of paths in a topological group. The additive version is probably more useful.

                            Equations
                            • γ₁.mul γ₂ = (γ₁.prod γ₂).map
                            Instances For
                              theorem Path.add_apply {X : Type u_1} [TopologicalSpace X] [Add X] [ContinuousAdd X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (t : unitInterval) :
                              (γ₁.add γ₂) t = γ₁ t + γ₂ t
                              theorem Path.mul_apply {X : Type u_1} [TopologicalSpace X] [Mul X] [ContinuousMul X] {a₁ : X} {b₁ : X} {a₂ : X} {b₂ : X} (γ₁ : Path a₁ b₁) (γ₂ : Path a₂ b₂) (t : unitInterval) :
                              (γ₁.mul γ₂) t = γ₁ t * γ₂ t

                              Truncating a path #

                              def Path.truncate {X : Type u_4} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t₀ : ) (t₁ : ) :
                              Path (γ.extend (min t₀ t₁)) (γ.extend t₁)

                              γ.truncate t₀ t₁ is the path which follows the path γ on the time interval [t₀, t₁] and stays still otherwise.

                              Equations
                              • γ.truncate t₀ t₁ = { toFun := fun (s : unitInterval) => γ.extend (min (max (s) t₀) t₁), continuous_toFun := , source' := , target' := }
                              Instances For
                                def Path.truncateOfLE {X : Type u_4} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t₀ : } {t₁ : } (h : t₀ t₁) :
                                Path (γ.extend t₀) (γ.extend t₁)

                                γ.truncateOfLE t₀ t₁ h, where h : t₀ ≤ t₁ is γ.truncate t₀ t₁ casted as a path from γ.extend t₀ to γ.extend t₁.

                                Equations
                                • γ.truncateOfLE h = (γ.truncate t₀ t₁).cast
                                Instances For
                                  theorem Path.truncate_range {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) {t₀ : } {t₁ : } :
                                  Set.range (γ.truncate t₀ t₁) Set.range γ
                                  theorem Path.truncate_continuous_family {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
                                  Continuous fun (x : × × unitInterval) => (γ.truncate x.1 x.2.1) x.2.2

                                  For a path γ, γ.truncate gives a "continuous family of paths", by which we mean the uncurried function which maps (t₀, t₁, s) to γ.truncate t₀ t₁ s is continuous.

                                  theorem Path.truncate_const_continuous_family {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : ) :
                                  Continuous (γ.truncate t)
                                  @[simp]
                                  theorem Path.truncate_self {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) (t : ) :
                                  γ.truncate t t = (Path.refl (γ.extend t)).cast
                                  @[simp]
                                  theorem Path.truncate_zero_zero {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
                                  γ.truncate 0 0 = (Path.refl a).cast
                                  @[simp]
                                  theorem Path.truncate_one_one {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
                                  γ.truncate 1 1 = (Path.refl b).cast
                                  @[simp]
                                  theorem Path.truncate_zero_one {X : Type u_1} [TopologicalSpace X] {a : X} {b : X} (γ : Path a b) :
                                  γ.truncate 0 1 = γ.cast

                                  Reparametrising a path #

                                  def Path.reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) (f : unitIntervalunitInterval) (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
                                  Path x y

                                  Given a path γ and a function f : I → I where f 0 = 0 and f 1 = 1, γ.reparam f is the path defined by γ ∘ f.

                                  Equations
                                  • γ.reparam f hfcont hf₀ hf₁ = { toFun := γ f, continuous_toFun := , source' := , target' := }
                                  Instances For
                                    @[simp]
                                    theorem Path.coe_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {f : unitIntervalunitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
                                    (γ.reparam f hfcont hf₀ hf₁) = γ f
                                    @[simp]
                                    theorem Path.reparam_id {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) :
                                    γ.reparam id = γ
                                    theorem Path.range_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (γ : Path x y) {f : unitIntervalunitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
                                    Set.range (γ.reparam f hfcont hf₀ hf₁) = Set.range γ
                                    theorem Path.refl_reparam {X : Type u_1} [TopologicalSpace X] {x : X} {f : unitIntervalunitInterval} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
                                    (Path.refl x).reparam f hfcont hf₀ hf₁ = Path.refl x

                                    Being joined by a path #

                                    def Joined {X : Type u_1} [TopologicalSpace X] (x : X) (y : X) :

                                    The relation "being joined by a path". This is an equivalence relation.

                                    Equations
                                    Instances For
                                      theorem Joined.refl {X : Type u_1} [TopologicalSpace X] (x : X) :
                                      Joined x x
                                      def Joined.somePath {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Joined x y) :
                                      Path x y

                                      When two points are joined, choose some path from x to y.

                                      Equations
                                      Instances For
                                        theorem Joined.symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : Joined x y) :
                                        Joined y x
                                        theorem Joined.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (hxy : Joined x y) (hyz : Joined y z) :
                                        Joined x z
                                        def pathSetoid (X : Type u_1) [TopologicalSpace X] :

                                        The setoid corresponding the equivalence relation of being joined by a continuous path.

                                        Equations
                                        Instances For
                                          def ZerothHomotopy (X : Type u_1) [TopologicalSpace X] :
                                          Type u_1

                                          The quotient type of points of a topological space modulo being joined by a continuous path.

                                          Equations
                                          Instances For

                                            Being joined by a path inside a set #

                                            def JoinedIn {X : Type u_1} [TopologicalSpace X] (F : Set X) (x : X) (y : X) :

                                            The relation "being joined by a path in F". Not quite an equivalence relation since it's not reflexive for points that do not belong to F.

                                            Equations
                                            Instances For
                                              theorem JoinedIn.mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                              x F y F
                                              theorem JoinedIn.source_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                              x F
                                              theorem JoinedIn.target_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                              y F
                                              def JoinedIn.somePath {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                              Path x y

                                              When x and y are joined in F, choose a path from x to y inside F

                                              Equations
                                              Instances For
                                                theorem JoinedIn.somePath_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) (t : unitInterval) :
                                                h.somePath t F
                                                theorem JoinedIn.joined_subtype {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                                Joined x, y,

                                                If x and y are joined in the set F, then they are joined in the subtype F.

                                                theorem JoinedIn.ofLine {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} {f : X} (hf : ContinuousOn f unitInterval) (h₀ : f 0 = x) (h₁ : f 1 = y) (hF : f '' unitInterval F) :
                                                JoinedIn F x y
                                                theorem JoinedIn.joined {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                                Joined x y
                                                theorem joinedIn_iff_joined {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (x_in : x F) (y_in : y F) :
                                                JoinedIn F x y Joined x, x_in y, y_in
                                                @[simp]
                                                theorem joinedIn_univ {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
                                                JoinedIn Set.univ x y Joined x y
                                                theorem JoinedIn.mono {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {U : Set X} {V : Set X} (h : JoinedIn U x y) (hUV : U V) :
                                                JoinedIn V x y
                                                theorem JoinedIn.refl {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : x F) :
                                                JoinedIn F x x
                                                theorem JoinedIn.symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : JoinedIn F x y) :
                                                JoinedIn F y x
                                                theorem JoinedIn.trans {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} {F : Set X} (hxy : JoinedIn F x y) (hyz : JoinedIn F y z) :
                                                JoinedIn F x z
                                                theorem Specializes.joinedIn {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : x y) (hx : x F) (hy : y F) :
                                                JoinedIn F x y
                                                theorem Inseparable.joinedIn {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : Inseparable x y) (hx : x F) (hy : y F) :
                                                JoinedIn F x y

                                                Path component #

                                                def pathComponent {X : Type u_1} [TopologicalSpace X] (x : X) :
                                                Set X

                                                The path component of x is the set of points that can be joined to x.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem mem_pathComponent_self {X : Type u_1} [TopologicalSpace X] (x : X) :
                                                  @[simp]
                                                  theorem pathComponent.nonempty {X : Type u_1} [TopologicalSpace X] (x : X) :
                                                  (pathComponent x).Nonempty
                                                  theorem mem_pathComponent_of_mem {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : x pathComponent y) :
                                                  theorem pathComponent_symm {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} :
                                                  theorem pathComponent_congr {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} (h : x pathComponent y) :
                                                  def pathComponentIn {X : Type u_1} [TopologicalSpace X] (x : X) (F : Set X) :
                                                  Set X

                                                  The path component of x in F is the set of points that can be joined to x in F.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem pathComponentIn_univ {X : Type u_1} [TopologicalSpace X] (x : X) :
                                                    theorem Joined.mem_pathComponent {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {z : X} (hyz : Joined y z) (hxy : y pathComponent x) :

                                                    Path connected sets #

                                                    def IsPathConnected {X : Type u_1} [TopologicalSpace X] (F : Set X) :

                                                    A set F is path connected if it contains a point that can be joined to all other in F.

                                                    Equations
                                                    Instances For
                                                      theorem isPathConnected_iff_eq {X : Type u_1} [TopologicalSpace X] {F : Set X} :
                                                      IsPathConnected F xF, pathComponentIn x F = F
                                                      theorem IsPathConnected.joinedIn {X : Type u_1} [TopologicalSpace X] {F : Set X} (h : IsPathConnected F) (x : X) :
                                                      x FyF, JoinedIn F x y
                                                      theorem isPathConnected_iff {X : Type u_1} [TopologicalSpace X] {F : Set X} :
                                                      IsPathConnected F F.Nonempty xF, yF, JoinedIn F x y
                                                      theorem IsPathConnected.image' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} (hF : IsPathConnected F) {f : XY} (hf : ContinuousOn f F) :

                                                      If f is continuous on F and F is path-connected, so is f(F).

                                                      theorem IsPathConnected.image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} (hF : IsPathConnected F) {f : XY} (hf : Continuous f) :

                                                      If f is continuous and F is path-connected, so is f(F).

                                                      theorem Inducing.isPathConnected_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {F : Set X} {f : XY} (hf : Inducing f) :

                                                      If f : X → Y is a Inducing, f(F) is path-connected iff F is.

                                                      @[simp]

                                                      If h : X → Y is a homeomorphism, h(s) is path-connected iff s is.

                                                      @[simp]

                                                      If h : X → Y is a homeomorphism, h⁻¹(s) is path-connected iff s is.

                                                      theorem IsPathConnected.mem_pathComponent {X : Type u_1} [TopologicalSpace X] {x : X} {y : X} {F : Set X} (h : IsPathConnected F) (x_in : x F) (y_in : y F) :
                                                      theorem IsPathConnected.subset_pathComponent {X : Type u_1} [TopologicalSpace X] {x : X} {F : Set X} (h : IsPathConnected F) (x_in : x F) :
                                                      theorem IsPathConnected.union {X : Type u_1} [TopologicalSpace X] {U : Set X} {V : Set X} (hU : IsPathConnected U) (hV : IsPathConnected V) (hUV : (U V).Nonempty) :
                                                      theorem IsPathConnected.preimage_coe {X : Type u_1} [TopologicalSpace X] {U : Set X} {W : Set X} (hW : IsPathConnected W) (hWU : W U) :
                                                      IsPathConnected (Subtype.val ⁻¹' W)

                                                      If a set W is path-connected, then it is also path-connected when seen as a set in a smaller ambient type U (when U contains W).

                                                      theorem IsPathConnected.exists_path_through_family {X : Type u_1} [TopologicalSpace X] {n : } {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1)X) (hp : ∀ (i : Fin (n + 1)), p i s) :
                                                      ∃ (γ : Path (p 0) (p n)), Set.range γ s ∀ (i : Fin (n + 1)), p i Set.range γ
                                                      theorem IsPathConnected.exists_path_through_family' {X : Type u_1} [TopologicalSpace X] {n : } {s : Set X} (h : IsPathConnected s) (p : Fin (n + 1)X) (hp : ∀ (i : Fin (n + 1)), p i s) :
                                                      ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1)unitInterval), (∀ (t : unitInterval), γ t s) ∀ (i : Fin (n + 1)), γ (t i) = p i

                                                      Path connected spaces #

                                                      A topological space is path-connected if it is non-empty and every two points can be joined by a continuous path.

                                                      • nonempty : Nonempty X

                                                        A path-connected space must be nonempty.

                                                      • joined : ∀ (x y : X), Joined x y

                                                        Any two points in a path-connected space must be joined by a continuous path.

                                                      Instances

                                                        A path-connected space must be nonempty.

                                                        theorem PathConnectedSpace.joined {X : Type u_4} [TopologicalSpace X] [self : PathConnectedSpace X] (x : X) (y : X) :
                                                        Joined x y

                                                        Any two points in a path-connected space must be joined by a continuous path.

                                                        def PathConnectedSpace.somePath {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] (x : X) (y : X) :
                                                        Path x y

                                                        Use path-connectedness to build a path between two points.

                                                        Equations
                                                        Instances For

                                                          This is a special case of NormedSpace.instPathConnectedSpace (and TopologicalAddGroup.pathConnectedSpace). It exists only to simplify dependencies.

                                                          Equations
                                                          @[instance 100]
                                                          Equations
                                                          • =
                                                          theorem PathConnectedSpace.exists_path_through_family {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {n : } (p : Fin (n + 1)X) :
                                                          ∃ (γ : Path (p 0) (p n)), ∀ (i : Fin (n + 1)), p i Set.range γ
                                                          theorem PathConnectedSpace.exists_path_through_family' {X : Type u_1} [TopologicalSpace X] [PathConnectedSpace X] {n : } (p : Fin (n + 1)X) :
                                                          ∃ (γ : Path (p 0) (p n)) (t : Fin (n + 1)unitInterval), ∀ (i : Fin (n + 1)), γ (t i) = p i

                                                          Locally path connected spaces #

                                                          A topological space is locally path connected, at every point, path connected neighborhoods form a neighborhood basis.

                                                          • path_connected_basis : ∀ (x : X), (nhds x).HasBasis (fun (s : Set X) => s nhds x IsPathConnected s) id

                                                            Each neighborhood filter has a basis of path-connected neighborhoods.

                                                          Instances
                                                            theorem LocPathConnectedSpace.path_connected_basis {X : Type u_4} [TopologicalSpace X] [self : LocPathConnectedSpace X] (x : X) :
                                                            (nhds x).HasBasis (fun (s : Set X) => s nhds x IsPathConnected s) id

                                                            Each neighborhood filter has a basis of path-connected neighborhoods.

                                                            theorem locPathConnected_of_bases {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {p : ιProp} {s : XιSet X} (h : ∀ (x : X), (nhds x).HasBasis p (s x)) (h' : ∀ (x : X) (i : ι), p iIsPathConnected (s x i)) :
                                                            theorem pathConnected_subset_basis {X : Type u_1} [TopologicalSpace X] {x : X} [LocPathConnectedSpace X] {U : Set X} (h : IsOpen U) (hx : x U) :
                                                            (nhds x).HasBasis (fun (s : Set X) => s nhds x IsPathConnected s s U) id