case h
𝕜 : Type u_1
E : Type ?u.288872
F : Type ?u.288875
β : Type ?u.288878
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ (x : ι), {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
𝕜 : Type u_1
E : Type ?u.288872
F : Type ?u.288875
β : Type ?u.288878
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ stdSimplex 𝕜 ι = (⋂ (x : ι), {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
ext f
no goals
case h
𝕜 : Type u_1
E : Type ?u.288872
F : Type ?u.288875
β : Type ?u.288878
ι : Type u_2
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ (x : ι), {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]