Documentation

Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex

The standard simplex is path-connected #

source
theorem Convexity.StdSimplex.continuous_convexCombPair {M : Type u_1} (x y : StdSimplex ℝ M) :
Continuous fun (t : ↑unitInterval) => convexCombPair ↑(unitInterval.symm t) ↑t ⋯ ⋯ ⋯ x y
source
theorem Convexity.StdSimplex.continuous_duple {M : Type u_1} (x y : M) :
Continuous fun (t : ↑unitInterval) => duple x y ⋯ ⋯ ⋯
source
instance Convexity.StdSimplex.pathConnectedSpace (M : Type u_1) [Nonempty M] :
PathConnectedSpace (StdSimplex ℝ M)
source
noncomputable def Convexity.StdSimplex.homeomorphI :
StdSimplex ℝ (Fin 2) ≃ₜ ↑unitInterval

The standard one-dimensional simplex is homeomorphic to the unit interval.

Instances For
    source
    theorem Convexity.StdSimplex.homeomorphI_apply_coe (s : StdSimplex ℝ (Fin 2)) :
    ↑(homeomorphI s) = s.weights 1
    source
    @[simp]
    theorem Convexity.StdSimplex.homeomorphI_single_zero :
    homeomorphI (single 0) = 0
    source
    @[simp]
    theorem Convexity.StdSimplex.homeomorphI_single_one :
    homeomorphI (single 1) = 1
    source
    @[simp]
    theorem Convexity.StdSimplex.homeomorphI_symm_zero :
    homeomorphI.symm 0 = single 0
    source
    @[simp]
    theorem Convexity.StdSimplex.homeomorphI_symm_one :
    homeomorphI.symm 1 = single 1