← Copula mathematical handbook

The standard simplex is compact

theorem Convexity.StdSimplex.range_toFun_comp_weights_subset_closedBall (M : Type u_1) [Fintype M] : (Set.range fun (t : StdSimplex ℝ M) => ⇑t.weights) ⊆ Metric.closedBall 0 1

theorem Convexity.StdSimplex.isBounded_range_toFun_comp_weights (M : Type u_1) [Finite M] : Bornology.IsBounded (Set.range fun (t : StdSimplex ℝ M) => ⇑t.weights)

theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall (M : Type u_1) [Fintype M] : Metric.diam (Set.range fun (t : StdSimplex ℝ M) => ⇑t.weights) ≤ 1

theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_zero (M : Type u_1) [Fintype M] [Subsingleton M] : Metric.diam (Set.range fun (t : StdSimplex ℝ M) => ⇑t.weights) = 0

theorem Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_one (M : Type u_1) [Fintype M] [Nontrivial M] : Metric.diam (Set.range fun (t : StdSimplex ℝ M) => ⇑t.weights) = 1

instance Convexity.StdSimplex.compactSpace (R : Type u_1) (M : Type u_2) [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [PartialOrder R] [IsStrictOrderedRing R] [CompactIccSpace R] [OrderClosedTopology R] [Finite M] : CompactSpace (StdSimplex R M)