ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ f ∈ closedBall 0 1
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
⊢ stdSimplex ℝ ι ⊆ closedBall 0 1
intro f hf
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (OfNat.ofNat 0 b) ≤ 1
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ f ∈ closedBall 0 1
rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (OfNat.ofNat 0 x) ≤ 1
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
⊢ ∀ (b : ι), dist (f b) (OfNat.ofNat 0 b) ≤ 1
intro x
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ dist (f x) (OfNat.ofNat 0 x) ≤ 1
rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
no goals
ι : Type u_1
𝕜 : Type ?u.492
E : Type ?u.495
inst✝ : Fintype ι
f : ι → ℝ
hf : f ∈ stdSimplex ℝ ι
x : ι
⊢ f x ≤ 1
exact (mem_Icc_of_mem_stdSimplex hf x).2