Convex sets and functions in vector spaces #
In a π-vector space, we define the following objects and properties.
convex π s: A setsis convex if for any two pointsx y β sit includessegment π x y.std_simplex π ΞΉ: The standard simplex inΞΉ β π(currently requiresfintype ΞΉ). It is the intersection of the positive quadrant with the hyperplanes.sum = 1.
We also provide various equivalent versions of the definitions above, prove that some specific sets are convex.
TODO #
Generalize all this file to affine spaces.
Convexity of sets #
def
convex
(π : Type u_1)
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
(s : set E) :
Prop
Convexity of sets.
Equations
- convex π s = β β¦x : Eβ¦, x β s β star_convex π x s
theorem
convex.star_convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E}
{x : E}
(hs : convex π s)
(hx : x β s) :
star_convex π x s
theorem
convex_iff_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E} :
theorem
convex.segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E}
(h : convex π s)
{x y : E}
(hx : x β s)
(hy : y β s) :
theorem
convex.open_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E}
(h : convex π s)
{x y : E}
(hx : x β s)
(hy : y β s) :
open_segment π x y β s
theorem
convex_iff_pointwise_add_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E} :
Alternative definition of set convexity, in terms of pointwise set operations.
theorem
convex.set_combo_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s : set E} :
Alias of the forward direction of convex_iff_pointwise_add_subset.
theorem
convex_empty
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E] :
theorem
convex_univ
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E] :
theorem
convex.inter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{s t : set E}
(hs : convex π s)
(ht : convex π t) :
theorem
convex_sInter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{S : set (set E)}
(h : β (s : set E), s β S β convex π s) :
theorem
convex_Inter
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{ΞΉ : Sort u_3}
{s : ΞΉ β set E}
(h : β (i : ΞΉ), convex π (s i)) :
convex π (β (i : ΞΉ), s i)
theorem
convex_Interβ
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{ΞΉ : Sort u_3}
{ΞΊ : ΞΉ β Sort u_4}
{s : Ξ (i : ΞΉ), ΞΊ i β set E}
(h : β (i : ΞΉ) (j : ΞΊ i), convex π (s i j)) :
convex π (β (i : ΞΉ) (j : ΞΊ i), s i j)
theorem
convex.prod
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[has_smul π E]
[has_smul π F]
{s : set E}
{t : set F}
(hs : convex π s)
(ht : convex π t) :
theorem
directed.convex_Union
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{ΞΉ : Sort u_3}
{s : ΞΉ β set E}
(hdir : directed has_subset.subset s)
(hc : β β¦i : ΞΉβ¦, convex π (s i)) :
convex π (β (i : ΞΉ), s i)
theorem
directed_on.convex_sUnion
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[has_smul π E]
{c : set (set E)}
(hdir : directed_on has_subset.subset c)
(hc : β β¦A : set Eβ¦, A β c β convex π A) :
theorem
convex_iff_open_segment_subset
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E} :
theorem
convex.star_convex_iff
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
{x : E}
(hs : convex π s)
(h : s.nonempty) :
star_convex π x s β x β s
@[protected]
theorem
set.subsingleton.convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(h : s.subsingleton) :
convex π s
theorem
convex_singleton
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(c : E) :
convex π {c}
theorem
convex_segment
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(x y : E) :
theorem
convex_open_segment
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(a b : E) :
convex π (open_segment π a b)
theorem
convex.linear_image
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
{s : set E}
(hs : convex π s)
(f : E ββ[π] F) :
theorem
convex.is_linear_image
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
{s : set E}
(hs : convex π s)
{f : E β F}
(hf : is_linear_map π f) :
theorem
convex.linear_preimage
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
{s : set F}
(hs : convex π s)
(f : E ββ[π] F) :
theorem
convex.is_linear_preimage
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring π]
[add_comm_monoid E]
[add_comm_monoid F]
[module π E]
[module π F]
{s : set F}
(hs : convex π s)
{f : E β F}
(hf : is_linear_map π f) :
theorem
convex.add
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s t : set E}
(hs : convex π s)
(ht : convex π t) :
theorem
convex.vadd
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(z : E) :
theorem
convex.translate
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(z : E) :
theorem
convex.translate_preimage_right
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(z : E) :
The translation of a convex set is also convex.
theorem
convex.translate_preimage_left
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(z : E) :
The translation of a convex set is also convex.
theorem
convex_Iic
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r : Ξ²) :
theorem
convex_Ici
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r : Ξ²) :
theorem
convex_Icc
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r s : Ξ²) :
theorem
convex_halfspace_le
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
{f : E β Ξ²}
(h : is_linear_map π f)
(r : Ξ²) :
theorem
convex_halfspace_ge
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
{f : E β Ξ²}
(h : is_linear_map π f)
(r : Ξ²) :
theorem
convex_hyperplane
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
[ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
{f : E β Ξ²}
(h : is_linear_map π f)
(r : Ξ²) :
theorem
convex_Iio
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r : Ξ²) :
theorem
convex_Ioi
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r : Ξ²) :
theorem
convex_Ioo
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r s : Ξ²) :
theorem
convex_Ico
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r s : Ξ²) :
theorem
convex_Ioc
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r s : Ξ²) :
theorem
convex_halfspace_lt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
{f : E β Ξ²}
(h : is_linear_map π f)
(r : Ξ²) :
theorem
convex_halfspace_gt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
[ordered_cancel_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
{f : E β Ξ²}
(h : is_linear_map π f)
(r : Ξ²) :
theorem
convex_interval
{π : Type u_1}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid Ξ²]
[module π Ξ²]
[ordered_smul π Ξ²]
(r s : Ξ²) :
convex π (set.interval r s)
theorem
monotone_on.convex_le
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : monotone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
monotone_on.convex_lt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : monotone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
monotone_on.convex_ge
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : monotone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
monotone_on.convex_gt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : monotone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
antitone_on.convex_le
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : antitone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
antitone_on.convex_lt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : antitone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
antitone_on.convex_ge
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : antitone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
antitone_on.convex_gt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{s : set E}
{f : E β Ξ²}
(hf : antitone_on f s)
(hs : convex π s)
(r : Ξ²) :
theorem
monotone.convex_le
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : monotone f)
(r : Ξ²) :
theorem
monotone.convex_lt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : monotone f)
(r : Ξ²) :
theorem
monotone.convex_ge
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : monotone f)
(r : Ξ²) :
theorem
monotone.convex_gt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : monotone f)
(r : Ξ²) :
theorem
antitone.convex_le
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : antitone f)
(r : Ξ²) :
theorem
antitone.convex_lt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : antitone f)
(r : Ξ²) :
theorem
antitone.convex_ge
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : antitone f)
(r : Ξ²) :
theorem
antitone.convex_gt
{π : Type u_1}
{E : Type u_2}
{Ξ² : Type u_4}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[ordered_add_comm_monoid Ξ²]
[module π E]
[ordered_smul π E]
{f : E β Ξ²}
(hf : antitone f)
(r : Ξ²) :
theorem
convex.smul
{π : Type u_1}
{E : Type u_2}
[ordered_comm_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(c : π) :
theorem
convex.smul_preimage
{π : Type u_1}
{E : Type u_2}
[ordered_comm_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(c : π) :
theorem
convex.affinity
{π : Type u_1}
{E : Type u_2}
[ordered_comm_semiring π]
[add_comm_monoid E]
[module π E]
{s : set E}
(hs : convex π s)
(z : E)
(c : π) :
theorem
convex.add_smul_mem
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(hs : convex π s)
{x y : E}
(hx : x β s)
(hy : x + y β s)
{t : π}
(ht : t β set.Icc 0 1) :
theorem
convex.smul_mem_of_zero_mem
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(hs : convex π s)
{x : E}
(zero_mem : 0 β s)
(hx : x β s)
{t : π}
(ht : t β set.Icc 0 1) :
theorem
convex.add_smul_sub_mem
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(h : convex π s)
{x y : E}
(hx : x β s)
(hy : y β s)
{t : π}
(ht : t β set.Icc 0 1) :
theorem
affine_subspace.convex
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
(Q : affine_subspace π E) :
Affine subspaces are convex.
theorem
convex.affine_preimage
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_ring π]
[add_comm_group E]
[add_comm_group F]
[module π E]
[module π F]
(f : E βα΅[π] F)
{s : set F}
(hs : convex π s) :
The preimage of a convex set under an affine map is convex.
theorem
convex.affine_image
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_ring π]
[add_comm_group E]
[add_comm_group F]
[module π E]
[module π F]
{s : set E}
(f : E βα΅[π] F)
(hs : convex π s) :
The image of a convex set under an affine map is convex.
theorem
convex.neg
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s : set E}
(hs : convex π s) :
theorem
convex.sub
{π : Type u_1}
{E : Type u_2}
[ordered_ring π]
[add_comm_group E]
[module π E]
{s t : set E}
(hs : convex π s)
(ht : convex π t) :
theorem
convex_iff_div
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{s : set E} :
Alternative definition of set convexity, using division.
theorem
convex.mem_smul_of_zero_mem
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{s : set E}
(h : convex π s)
{x : E}
(zero_mem : 0 β s)
(hx : x β s)
{t : π}
(ht : 1 β€ t) :
theorem
convex.add_smul
{π : Type u_1}
{E : Type u_2}
[linear_ordered_field π]
[add_comm_group E]
[module π E]
{s : set E}
(h_conv : convex π s)
{p q : π}
(hp : 0 β€ p)
(hq : 0 β€ q) :
theorem
set.ord_connected.convex_of_chain
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{s : set E}
(hs : s.ord_connected)
(h : is_chain has_le.le s) :
convex π s
theorem
set.ord_connected.convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[linear_ordered_add_comm_monoid E]
[module π E]
[ordered_smul π E]
{s : set E}
(hs : s.ord_connected) :
convex π s
theorem
convex_iff_ord_connected
{π : Type u_1}
[linear_ordered_field π]
{s : set π} :
convex π s β s.ord_connected
theorem
convex.ord_connected
{π : Type u_1}
[linear_ordered_field π]
{s : set π} :
convex π s β s.ord_connected
Alias of the forward direction of convex_iff_ord_connected.
Convexity of submodules/subspaces #
@[protected]
theorem
submodule.convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(K : submodule π E) :
@[protected]
theorem
submodule.star_convex
{π : Type u_1}
{E : Type u_2}
[ordered_semiring π]
[add_comm_monoid E]
[module π E]
(K : submodule π E) :
star_convex π 0 βK
Simplex #
def
std_simplex
(π : Type u_1)
(ΞΉ : Type u_5)
[ordered_semiring π]
[fintype ΞΉ] :
set (ΞΉ β π)
The standard simplex in the space of functions ΞΉ β π is the set of vectors with non-negative
coordinates with total sum 1. This is the free object in the category of convex spaces.
Equations
- std_simplex π ΞΉ = {f : ΞΉ β π | (β (x : ΞΉ), 0 β€ f x) β§ finset.univ.sum (Ξ» (x : ΞΉ), f x) = 1}
theorem
std_simplex_eq_inter
(π : Type u_1)
(ΞΉ : Type u_5)
[ordered_semiring π]
[fintype ΞΉ] :
std_simplex π ΞΉ = (β (x : ΞΉ), {f : ΞΉ β π | 0 β€ f x}) β© {f : ΞΉ β π | finset.univ.sum (Ξ» (x : ΞΉ), f x) = 1}
theorem
convex_std_simplex
(π : Type u_1)
(ΞΉ : Type u_5)
[ordered_semiring π]
[fintype ΞΉ] :
convex π (std_simplex π ΞΉ)
theorem
ite_eq_mem_std_simplex
(π : Type u_1)
{ΞΉ : Type u_5}
[ordered_semiring π]
[fintype ΞΉ]
(i : ΞΉ) :
(Ξ» (j : ΞΉ), ite (i = j) 1 0) β std_simplex π ΞΉ