Bridge coercions from PiecewiseC1Curve to mathlib Path / ContinuousMap

We provide PiecewiseC1Curve.toPath and PiecewiseC1Curve.toContinuousMap that rescale the domain [a,b] to the unit interval [0,1] via iccHomeoI.

noncomputable def PiecewiseC1Curve.rescale (γ : PiecewiseC1Curve) : ↑unitInterval → ↑(Set.Icc γ.a γ.b)

The rescaling homeomorphism from I = [0,1] to [a,b], as a subtype-valued map.

Equations

• γ.rescale = ⇑(iccHomeoI γ.a γ.b ⋯).symm

noncomputable def PiecewiseC1Curve.toPath (γ : PiecewiseC1Curve) : Path (γ.toFun γ.a) (γ.toFun γ.b)

Convert a PiecewiseC1Curve to a mathlib Path by rescaling [a,b] to [0,1]. The path goes from γ(a) to γ(b).

Equations

• γ.toPath = { toFun := fun (t : ↑unitInterval) => γ.toFun ↑(γ.rescale t), continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

noncomputable def PiecewiseC1Curve.toContinuousMap (γ : PiecewiseC1Curve) : C(↑unitInterval, ℂ)

Convert a PiecewiseC1Curve to a ContinuousMap from the unit interval to ℂ.

Equations

• γ.toContinuousMap = γ.toPath.toContinuousMap

theorem PiecewiseC1Curve.toPath_apply (γ : PiecewiseC1Curve) (t : ↑unitInterval) : γ.toPath t = γ.toFun ↑((iccHomeoI γ.a γ.b ⋯).symm t)

toPath agrees with the original curve under rescaling.

theorem PiecewiseC1Curve.toContinuousMap_apply (γ : PiecewiseC1Curve) (t : ↑unitInterval) : γ.toContinuousMap t = γ.toFun ↑((iccHomeoI γ.a γ.b ⋯).symm t)

toContinuousMap agrees with the original curve under rescaling.

noncomputable def PiecewiseC1Curve.toLoop (γ : PiecewiseC1Curve) (hc : γ.IsClosed) : Path (γ.toFun γ.a) (γ.toFun γ.a)

A closed PiecewiseC1Curve gives a loop, i.e., a Path from γ(a) to itself.

Equations

• γ.toLoop hc = γ.toPath.cast ⋯ hc