English
The image under a linear map of the standard simplex is contained in the standard simplex of the target space.
Русский
Образ под линейным отображением стандартного симплекса содержится в стандартном симплексe целевого пространства.
LaTeX
$$For any linear map $f$, $\mathrm{image}(\mathrm{linearMap}\; f)(\mathrm{stdSimplex}\; S\; X) \subseteq \mathrm{stdSimplex}\; S\; Y$$$
Lean4
theorem image_linearMap (f : X → Y) : Set.image (FunOnFinite.linearMap S S f) (stdSimplex S X) ⊆ stdSimplex S Y := by
classical
rintro _ ⟨s, ⟨hs₀, hs₁⟩, rfl⟩
refine ⟨fun y ↦ ?_, ?_⟩
· rw [FunOnFinite.linearMap_apply_apply]
exact Finset.sum_nonneg (by aesop)
· simp only [FunOnFinite.linearMap_apply_apply, ← hs₁]
exact Finset.sum_fiberwise Finset.univ f s
