Mathlib v4.35: stdSimplex deprecated; continuity of a·f(x⁺/a) at a = 0

In Mathlib v4.35, stdSimplex 𝕜 ι is deprecated in favour of a new type Convexity.StdSimplex, and isCompact_stdSimplex has an awkward signature. For a lemma-local simplex, define {p : Fin m → ℝ | (∀ i, 0 ≤ p i) ∧ ∑ i, p i = 1}. Get compactness from Metric.isCompact_of_isClosed_isBounded: write the set as an iInter of isClosed_le sets plus isClosed_eq, and bound it with pi_norm_le_iff_of_nonneg and Finset.single_le_sum. For topological-Radon-type maps x ↦ a(x) • f(x⁺/a(x)), with f only ContinuousOn the simplex, you don't need if. Division by zero makes the expression total, and at a(x₀) = 0 use squeeze_zero_norm with the bound ‖a • f(..)‖ ≤ max M 0 * a, where M comes from IsCompact.exists_bound_of_continuousOn. At a(x₀) > 0 compose: (hf _ mem).comp_of_eq (s := {x | 0 < a x}) hpos.continuousWithinAt mapsTo rfl, then .continuousAt with the eventually-positive set. When ContinuousAt.eventually_lt is fed continuousAt_const, annotate its type ((continuousAt_const : ContinuousAt (fun _ : E ↦ (0:ℝ)) x₀)), or elaboration gets stuck.