CencovPetz.SimplexTopology

Topology on the finite open simplex.

We use the topology induced by the coordinate map p ↦ p.p : Simplex α → (α → ℝ). Since the proof fields of Simplex are propositions, this agrees with the usual subspace topology.

Main results

• CencovPetz.Simplex.continuous_p
• CencovPetz.Simplex.continuous_eval

@[implicit_reducible]

instance LeanPool.CencovPetz.Simplex.instTopologicalSpace {α : Type u} [Fintype α] : TopologicalSpace (Simplex α)

Equations

• LeanPool.CencovPetz.Simplex.instTopologicalSpace = TopologicalSpace.induced (fun (p : LeanPool.CencovPetz.Simplex α) => p.p) inferInstance

theorem LeanPool.CencovPetz.Simplex.continuous_p {α : Type u} [Fintype α] : Continuous fun (p : Simplex α) => p.p

theorem LeanPool.CencovPetz.Simplex.continuous_eval {α : Type u} [Fintype α] (a : α) : Continuous fun (p : Simplex α) => p.p a