StdSimplex

📁 Source: Mathlib/Analysis/Convex/StdSimplex.lean

Statistics

Metric	Count
Definitions StdSimplex, stdSimplex, barycenter, instFunLikeElemForall, instUniqueElemForall, map, vertex, stdSimplexEquivIcc, stdSimplexHomeomorphUnitInterval	9
Theorems convexHull_eq_image, bounded_stdSimplex, convexHull_basis_eq_stdSimplex, convexHull_rangle_single_eq_stdSimplex, convex_stdSimplex, diam_stdSimplex, diam_stdSimplex_le, diam_stdSimplex_of_subsingleton, instPathConnectedSpaceElemForallRealStdSimplexOfNonempty, isClosed_stdSimplex, isCompact_stdSimplex, isPathConnected_stdSimplex, ite_eq_mem_stdSimplex, mem_Icc_of_mem_stdSimplex, segment_single_subset_stdSimplex, single_mem_stdSimplex, add_eq_one, barycenter_apply, barycenter_eq_centerMass, continuous_map, eq_one_of_unique, ext, ext_iff, image_linearMap, instCompactSpace_coe, instNonemptyElemForall, instNontrivialElemForall, instSubsingletonElemForall, le_one, map_coe, map_comp_apply, map_id_apply, map_vertex, sum_eq_one, vertex_coe, vertex_injective, zero_le, stdSimplexEquivIcc_apply_coe, stdSimplexEquivIcc_one, stdSimplexEquivIcc_symm_apply_coe, stdSimplexEquivIcc_zero, stdSimplexHomeomorphUnitInterval_apply_coe, stdSimplexHomeomorphUnitInterval_one, stdSimplexHomeomorphUnitInterval_symm_apply_coe, stdSimplexHomeomorphUnitInterval_zero, stdSimplex_eq_inter, stdSimplex_fin_two, stdSimplex_of_isEmpty_index, stdSimplex_of_subsingleton, stdSimplex_subset_closedBall, stdSimplex_unique	51
Total	60

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull_eq_image 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid Set.image LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid Set.Elem NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.Function.module Semiring.toModule LinearMap.instFunLike Finset.sum LinearMap.addCommMonoid Finset.univ fintype LinearMap.smulRight IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.proj Set.instMembership stdSimplex	—	IsScalarTower.left convexHull_basis_eq_stdSimplex LinearMap.image_convexHull Set.range_comp LinearMap.coe_sum Finset.sum_congr Set.ext Finset.sum_apply ite_smul one_smul zero_smul Finset.sum_ite_eq

(root)

Definitions

Name	Category	Theorems
StdSimplex 📖	CompData	1 math math: ConvexSpace.assoc
stdSimplex 📖	CompOp	54 math math: isCompact_stdSimplex, stdSimplex_of_isEmpty_index, stdSimplexHomeomorphUnitInterval_symm_apply_coe, SimplexCategory.toTopObj_one_coe_add_coe_eq_one, stdSimplex_fin_two, stdSimplexHomeomorphUnitInterval_zero, stdSimplex_subset_closedBall, segment_single_subset_stdSimplex, SimplexCategory.continuous_toTopMap, instPathConnectedSpaceElemForallRealStdSimplexOfNonempty, diam_stdSimplex, single_mem_stdSimplex, stdSimplex.eq_one_of_unique, SimplexCategory.toTop_obj, convexHull_basis_eq_stdSimplex, SimplexCategory.toTop_map, stdSimplex.map_coe, ite_eq_mem_stdSimplex, SimplexCategory.toTop₀_map, isClosed_stdSimplex, SimplexCategory.toTop₀_obj, SimplexCategory.toTopObj_one_add_eq_one, diam_stdSimplex_of_subsingleton, stdSimplex.continuous_map, stdSimplex.vertex_coe, stdSimplex_of_subsingleton, diam_stdSimplex_le, bounded_stdSimplex, stdSimplex.ext_iff, stdSimplexHomeomorphUnitInterval_apply_coe, stdSimplex.instSubsingletonElemForall, stdSimplex.sum_eq_one, isPathConnected_stdSimplex, stdSimplex.instNonemptyElemForall, stdSimplex.barycenter_apply, stdSimplex.zero_le, convex_stdSimplex, stdSimplex.vertex_injective, stdSimplexHomeomorphUnitInterval_one, stdSimplex.add_eq_one, stdSimplex.image_linearMap, stdSimplex.barycenter_eq_centerMass, stdSimplexEquivIcc_apply_coe, Set.Finite.convexHull_eq_image, convexHull_rangle_single_eq_stdSimplex, stdSimplexEquivIcc_symm_apply_coe, stdSimplex.le_one, stdSimplex.instNontrivialElemForall, stdSimplexEquivIcc_one, stdSimplex.instCompactSpace_coe, stdSimplex_eq_inter, stdSimplex_unique, SimplexCategory.toTopObj_zero_apply_zero, stdSimplexEquivIcc_zero
stdSimplexEquivIcc 📖	CompOp	4 math math: stdSimplexEquivIcc_apply_coe, stdSimplexEquivIcc_symm_apply_coe, stdSimplexEquivIcc_one, stdSimplexEquivIcc_zero
stdSimplexHomeomorphUnitInterval 📖	CompOp	4 math math: stdSimplexHomeomorphUnitInterval_symm_apply_coe, stdSimplexHomeomorphUnitInterval_zero, stdSimplexHomeomorphUnitInterval_apply_coe, stdSimplexHomeomorphUnitInterval_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounded_stdSimplex 📖	mathematical	—	Bornology.IsBounded Pi.instBornology Real PseudoMetricSpace.toBornology Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder	—	Metric.isBounded_iff_subset_closedBall stdSimplex_subset_closedBall
convexHull_basis_eq_stdSimplex 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.Function.module Semiring.toModule Set.range AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass stdSimplex	—	Set.Subset.antisymm convexHull_min ite_eq_mem_stdSimplex IsStrictOrderedRing.toZeroLEOneClass convex_stdSimplex IsStrictOrderedRing.toIsOrderedRing pi_eq_sum_univ Finset.centerMass_eq_of_sum_1 Finset.centerMass_mem_convexHull zero_lt_one NeZero.charZero_one IsStrictOrderedRing.toCharZero Set.mem_range_self
convexHull_rangle_single_eq_stdSimplex 📖	mathematical	—	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Pi.Function.module Semiring.toModule Set.range Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing stdSimplex	—	Pi.single_eq_of_ne' Pi.single_eq_same convexHull_basis_eq_stdSimplex
convex_stdSimplex 📖	mathematical	—	Convex Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul stdSimplex	—	add_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono Finset.sum_congr Finset.sum_add_distrib Finset.smul_sum smul_eq_mul mul_one
diam_stdSimplex 📖	mathematical	—	Metric.diam pseudoMetricSpacePi Real Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder Real.instOne	—	le_antisymm diam_stdSimplex_le exists_pair_ne dist_single_single sub_zero abs_one Real.instIsOrderedRing max_self Metric.dist_le_diam_of_mem bounded_stdSimplex single_mem_stdSimplex Real.instZeroLEOneClass
diam_stdSimplex_le 📖	mathematical	—	Real Real.instLE Metric.diam pseudoMetricSpacePi Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder Real.instOne	—	Metric.diam_le_of_forall_dist_le zero_le_one Real.instZeroLEOneClass dist_pi_le_iff mem_Icc_of_mem_stdSimplex Real.instIsOrderedAddMonoid
diam_stdSimplex_of_subsingleton 📖	mathematical	—	Metric.diam pseudoMetricSpacePi Real Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder Real.instZero	—	isEmpty_or_nonempty stdSimplex_of_isEmpty_index Real.instNontrivial Metric.diam_empty stdSimplex_unique Real.instZeroLEOneClass Metric.diam_singleton
instPathConnectedSpaceElemForallRealStdSimplexOfNonempty 📖	mathematical	—	PathConnectedSpace Set.Elem stdSimplex Real Real.semiring Real.partialOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	isPathConnected_iff_pathConnectedSpace isPathConnected_stdSimplex
isClosed_stdSimplex 📖	mathematical	—	IsClosed Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder	—	IsClosed.inter isClosed_iInter isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal continuous_const continuous_apply isClosed_eq TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity continuous_finset_sum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal stdSimplex_eq_inter
isCompact_stdSimplex 📖	mathematical	—	IsCompact Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder	—	Metric.isCompact_iff_isClosed_bounded Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space instOrderTopologyReal UniformSpace.pseudoMetrizableSpace EMetric.instIsCountablyGeneratedUniformity pi_properSpace instProperSpaceReal isClosed_stdSimplex bounded_stdSimplex
isPathConnected_stdSimplex 📖	mathematical	—	IsPathConnected Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace stdSimplex Real.semiring Real.partialOrder	—	Convex.isPathConnected instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal instContinuousSMulForall ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul convex_stdSimplex Real.instIsOrderedRing single_mem_stdSimplex Real.instZeroLEOneClass
ite_eq_mem_stdSimplex 📖	mathematical	—	Set Set.instMembership stdSimplex AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	single_mem_stdSimplex
mem_Icc_of_mem_stdSimplex 📖	mathematical	Set Set.instMembership stdSimplex	Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono Finset.mem_univ
segment_single_subset_stdSimplex 📖	mathematical	—	Set Set.instHasSubset segment Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne stdSimplex	—	Convex.segment_subset convex_stdSimplex single_mem_stdSimplex
single_mem_stdSimplex 📖	mathematical	—	Set Set.instMembership stdSimplex Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_update_iff zero_le_one le_rfl Finset.sum_pi_single'
stdSimplexEquivIcc_apply_coe 📖	mathematical	—	Set Set.instMembership Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe Equiv Set.Elem stdSimplex Ring.toSemiring Fin.fintype EquivLike.toFunLike Equiv.instEquivLike stdSimplexEquivIcc	—	—
stdSimplexEquivIcc_one 📖	mathematical	—	DFunLike.coe Equiv Set.Elem stdSimplex Ring.toSemiring Fin.fintype Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne EquivLike.toFunLike Equiv.instEquivLike stdSimplexEquivIcc Set Set.instMembership Pi.single NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single_mem_stdSimplex IsOrderedRing.toZeroLEOneClass Set.Icc.instOne	—	single_mem_stdSimplex IsOrderedRing.toZeroLEOneClass
stdSimplexEquivIcc_symm_apply_coe 📖	mathematical	—	Set Set.instMembership stdSimplex Ring.toSemiring Fin.fintype DFunLike.coe Equiv Set.Elem Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne EquivLike.toFunLike Equiv.instEquivLike Equiv.symm stdSimplexEquivIcc Matrix.vecCons SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Matrix.vecEmpty	—	—
stdSimplexEquivIcc_zero 📖	mathematical	—	DFunLike.coe Equiv Set.Elem stdSimplex Ring.toSemiring Fin.fintype Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne EquivLike.toFunLike Equiv.instEquivLike stdSimplexEquivIcc Set Set.instMembership Pi.single NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single_mem_stdSimplex IsOrderedRing.toZeroLEOneClass Set.Icc.instZero	—	single_mem_stdSimplex IsOrderedRing.toZeroLEOneClass
stdSimplexHomeomorphUnitInterval_apply_coe 📖	mathematical	—	Real Set Set.instMembership Set.Icc PartialOrder.toPreorder Real.partialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Real.instRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe Homeomorph Set.Elem stdSimplex Real.semiring Fin.fintype unitInterval instTopologicalSpaceSubtype Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike stdSimplexHomeomorphUnitInterval Ring.toSemiring	—	—
stdSimplexHomeomorphUnitInterval_one 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem stdSimplex Real Real.semiring Real.partialOrder Fin.fintype unitInterval instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike stdSimplexHomeomorphUnitInterval Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single_mem_stdSimplex Real.instZeroLEOneClass Set.Icc.instOne Real.instIsOrderedRing	—	single_mem_stdSimplex Real.instZeroLEOneClass
stdSimplexHomeomorphUnitInterval_symm_apply_coe 📖	mathematical	—	Set Set.instMembership stdSimplex Real Ring.toSemiring Real.instRing Real.partialOrder Fin.fintype DFunLike.coe Homeomorph Set.Elem unitInterval Real.semiring instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm stdSimplexHomeomorphUnitInterval Matrix.vecCons SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set.Icc PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Matrix.vecEmpty	—	—
stdSimplexHomeomorphUnitInterval_zero 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem stdSimplex Real Real.semiring Real.partialOrder Fin.fintype unitInterval instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace EquivLike.toFunLike Homeomorph.instEquivLike stdSimplexHomeomorphUnitInterval Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne single_mem_stdSimplex Real.instZeroLEOneClass Set.Icc.instZero Real.instIsOrderedRing	—	single_mem_stdSimplex Real.instZeroLEOneClass
stdSimplex_eq_inter 📖	mathematical	—	stdSimplex Set Set.instInter Set.iInter setOf Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Set.ext
stdSimplex_fin_two 📖	mathematical	—	stdSimplex Fin.fintype segment Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne	—	Set.Subset.antisymm Fin.sum_univ_two Pi.single_eq_same mul_one Pi.single_eq_of_ne Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero add_zero zero_add segment_single_subset_stdSimplex
stdSimplex_of_isEmpty_index 📖	mathematical	—	stdSimplex Set Set.instEmptyCollection	—	Set.eq_empty_of_forall_notMem Finset.sum_congr Finset.univ_eq_empty NeZero.one
stdSimplex_of_subsingleton 📖	mathematical	—	stdSimplex Set.univ	—	Set.eq_univ_of_forall Eq.le
stdSimplex_subset_closedBall 📖	mathematical	—	Set Set.instHasSubset stdSimplex Real Real.semiring Real.partialOrder Metric.closedBall pseudoMetricSpacePi Real.pseudoMetricSpace Pi.instZero Real.instZero Real.instOne	—	Metric.mem_closedBall dist_pi_le_iff zero_le_one Real.instZeroLEOneClass Pi.zero_apply Real.dist_0_eq_abs abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mem_Icc_of_mem_stdSimplex
stdSimplex_unique 📖	mathematical	—	stdSimplex Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	nonempty_unique Set.eq_singleton_iff_unique_mem zero_le_one Fintype.sum_unique Unique.forall_iff

stdSimplex

Definitions

Name	Category	Theorems
barycenter 📖	CompOp	2 math math: barycenter_apply, barycenter_eq_centerMass
instFunLikeElemForall 📖	CompOp	11 math math: SimplexCategory.toTopObj_one_coe_add_coe_eq_one, eq_one_of_unique, map_coe, SimplexCategory.toTopObj_one_add_eq_one, vertex_coe, ext_iff, sum_eq_one, zero_le, add_eq_one, le_one, SimplexCategory.toTopObj_zero_apply_zero
instUniqueElemForall 📖	CompOp	—
map 📖	CompOp	8 math math: SimplexCategory.continuous_toTopMap, SimplexCategory.toTop_map, map_coe, SimplexCategory.toTop₀_map, continuous_map, map_id_apply, map_comp_apply, map_vertex
vertex 📖	CompOp	3 math math: vertex_coe, vertex_injective, map_vertex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_one 📖	mathematical	—	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe Set.Elem stdSimplex Fin.fintype instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Fin.sum_univ_two sum_eq_one
barycenter_apply 📖	mathematical	—	Set Set.instMembership stdSimplex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder barycenter InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Fintype.card	—	—
barycenter_eq_centerMass 📖	mathematical	—	Set Set.instMembership stdSimplex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder barycenter Finset.centerMass Pi.addCommGroup Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Semiring.toModule Finset.univ AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	Finset.sum_congr Finset.sum_const nsmul_eq_mul mul_one one_smul Finset.sum_apply Pi.single_apply Finset.sum_ite_eq
continuous_map 📖	mathematical	—	Continuous Set.Elem stdSimplex instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace map	—	Finite.of_fintype Continuous.comp FunOnFinite.continuous_linearMap IsTopologicalSemiring.toContinuousAdd continuous_induced_dom
eq_one_of_unique 📖	mathematical	—	DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	instSubsingletonElemForall Unique.instSubsingleton
ext 📖	—	DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall	—	—	—
ext_iff 📖	mathematical	—	DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall	—	ext
image_linearMap 📖	mathematical	—	Set Set.instHasSubset Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike FunOnFinite.linearMap Finite.of_fintype stdSimplex	—	Finite.of_fintype FunOnFinite.linearMap_apply_apply Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Finset.sum_congr Finset.sum_fiberwise
instCompactSpace_coe 📖	mathematical	—	CompactSpace Set.Elem stdSimplex Real Real.semiring Real.partialOrder instTopologicalSpaceSubtype Set Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	isCompact_iff_compactSpace isCompact_stdSimplex
instNonemptyElemForall 📖	mathematical	—	Set.Elem stdSimplex	—	—
instNontrivialElemForall 📖	mathematical	—	Nontrivial Set.Elem stdSimplex	—	exists_pair_ne vertex_injective
instSubsingletonElemForall 📖	mathematical	—	Set.Elem stdSimplex	—	ext sum_eq_one Finset.sum_eq_single instIsEmptyFalse
le_one 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	sum_eq_one Finset.single_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
map_coe 📖	mathematical	—	DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall map LinearMap RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.instFunLike FunOnFinite.linearMap Finite.of_fintype	—	—
map_comp_apply 📖	mathematical	—	map	—	ext Finite.of_fintype RingHomCompTriple.ids FunOnFinite.linearMap_comp
map_id_apply 📖	mathematical	—	map	—	ext Finite.of_fintype FunOnFinite.linearMap_id
map_vertex 📖	mathematical	—	map vertex	—	ext Finite.of_fintype FunOnFinite.linearMap_piSingle
sum_eq_one 📖	mathematical	—	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finset.univ DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
vertex_coe 📖	mathematical	—	DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall vertex Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
vertex_injective 📖	mathematical	—	Set.Elem stdSimplex vertex	—	DFunLike.congr_fun Pi.single_eq_same Pi.single_eq_of_ne NeZero.one
zero_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe Set.Elem stdSimplex instFunLikeElemForall	—	—

---

← Back to Index