Loogle!

Result

Found 194 declarations mentioning Convexity.StdSimplex.

Convexity.StdSimplex 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
(R : Type u) [LE R] [AddCommMonoid R] [One R] (M : Type v) : Type (max u v)
Convexity.StdSimplex.weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [LE R] [AddCommMonoid R] [One R] {M : Type v} (self : Convexity.StdSimplex R M) : M →₀ R
Convexity.StdSimplex.instSubsingleton 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Subsingleton M] : Subsingleton (Convexity.StdSimplex R M)
Convexity.StdSimplex.nonempty 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : Convexity.StdSimplex R M) : Nonempty M
Convexity.StdSimplex.single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x : M) : Convexity.StdSimplex R M
Convexity.StdSimplex.instInhabited 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] [Inhabited M] : Inhabited (Convexity.StdSimplex R M)
Convexity.StdSimplex.instNonempty 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] [Nonempty M] : Nonempty (Convexity.StdSimplex R M)
Convexity.StdSimplex.instNontrivial 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] [Nontrivial M] : Nontrivial (Convexity.StdSimplex R M)
Convexity.StdSimplex.instUnique 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] [Unique M] : Unique (Convexity.StdSimplex R M)
Convexity.StdSimplex.instConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] : Convexity.ConvexSpace R (Convexity.StdSimplex R I)
Convexity.ConvexSpace.convexCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R M) : M
Convexity.ConvexSpace.sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R M) : M
Convexity.StdSimplex.single_injective 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] : Function.Injective Convexity.StdSimplex.single
Convexity.iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → M) : M
Convexity.StdSimplex.total 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [LE R] [AddCommMonoid R] [One R] {M : Type v} (self : Convexity.StdSimplex R M) : (self.weights.sum fun x r => r) = 1
Convexity.iConvexComb_const 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (m : M) : (Convexity.iConvexComb s fun x => m) = m
Convexity.StdSimplex.map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type v} {N : Type w} (g : M → N) (f : Convexity.StdSimplex R M) : Convexity.StdSimplex R N
Convexity.iConvexComb_id 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.iConvexComb w id = Convexity.sConvexComb w
Convexity.iConvexComb_id' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M) : (Convexity.iConvexComb w fun x => x) = Convexity.sConvexComb w
Convexity.StdSimplex.map_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] (x : M) (f : M → N) : Convexity.StdSimplex.map f (Convexity.StdSimplex.single x) = Convexity.StdSimplex.single (f x)
Convexity.StdSimplex.map_id 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) : Convexity.StdSimplex.map id f = f
Convexity.StdSimplex.support_weights_nonempty 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : Convexity.StdSimplex R M) : w.weights.support.Nonempty
Convexity.sConvexComb_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M) : Convexity.sConvexComb (Convexity.StdSimplex.map f w) = Convexity.iConvexComb w f
Convexity.StdSimplex.equivIcc 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : Convexity.StdSimplex R' (Fin 2) ≃ ↑(Set.Icc 0 1)
Convexity.StdSimplex.join 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : Convexity.StdSimplex R M
Convexity.StdSimplex.map_const 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (x : N) : Convexity.StdSimplex.map (fun x_1 => x) f = Convexity.StdSimplex.single x
Convexity.iConvexComb_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → J) (g : J → M) : Convexity.iConvexComb (Convexity.StdSimplex.map f s) g = Convexity.iConvexComb s fun i => g (f i)
Convexity.StdSimplex.isAffineMap_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
(R : Type u_1) {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : I → J) : Convexity.IsAffineMap R (Convexity.StdSimplex.map f)
Convexity.StdSimplex.map_id' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] : Convexity.StdSimplex.map id = id
Convexity.IsAffineMap.map_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (self : Convexity.IsAffineMap R f) (s : Convexity.StdSimplex R M) : f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)
Convexity.IsAffineMap.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (map_sConvexComb : ∀ (s : Convexity.StdSimplex R M), f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)) : Convexity.IsAffineMap R f
Convexity.IsAffineMap.map_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (hf : Convexity.IsAffineMap R f) (s : Convexity.StdSimplex R I) (g : I → M) : f (Convexity.iConvexComb s g) = Convexity.iConvexComb s (f ∘ g)
Convexity.StdSimplex.map_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : Convexity.StdSimplex.map g₂ (Convexity.StdSimplex.map g₁ f) = Convexity.StdSimplex.map (fun x => g₂ (g₁ x)) f
Convexity.StdSimplex.nonneg 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [LE R] [AddCommMonoid R] [One R] {M : Type v} (self : Convexity.StdSimplex R M) : 0 ≤ self.weights
Convexity.StdSimplex.map_comp 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R M) (g₁ : M → N) (g₂ : N → P) : Convexity.StdSimplex.map (g₂ ∘ g₁) f = Convexity.StdSimplex.map g₂ (Convexity.StdSimplex.map g₁ f)
Convexity.StdSimplex.iConvexComb_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (x : Convexity.StdSimplex R I) : Convexity.iConvexComb x Convexity.StdSimplex.single = x
Convexity.StdSimplex.weights_nonneg 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {w : Convexity.StdSimplex R M} (i : M) : 0 ≤ w.weights i
Convexity.StdSimplex.duple 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x y : M) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) : Convexity.StdSimplex R M
Convexity.StdSimplex.weights_apply_eq_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Subsingleton M] (s : Convexity.StdSimplex R M) (m : M) : s.weights m = 1
Convexity.StdSimplex.support_weights_eq_singleton 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {w : Convexity.StdSimplex R M} {x : M} [IsStrictOrderedRing R] : w.weights.support = {x} ↔ w = Convexity.StdSimplex.single x
Convexity.StdSimplex.weights_apply_le_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (s : Convexity.StdSimplex R M) (m : M) : s.weights m ≤ 1
Convexity.StdSimplex.weights_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type v} {N : Type w} (g : M → N) (f : Convexity.StdSimplex R M) : (Convexity.StdSimplex.map g f).weights = Finsupp.mapDomain g f.weights
Convexity.StdSimplex.total_of_fintype 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Fintype M] (w : Convexity.StdSimplex R M) : ∑ i, w.weights i = 1
Convexity.StdSimplex.weights_ne_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Nontrivial R] (w : Convexity.StdSimplex R M) : w.weights ≠ 0
Convexity.ConvexSpace.assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f) = Convexity.sConvexComb f.join
Convexity.iConvexComb_reindex 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I ≃ J) (g : I → M) : Convexity.iConvexComb s g = Convexity.iConvexComb (Convexity.StdSimplex.map (⇑f) s) (g ∘ ⇑f.symm)
Convexity.StdSimplex.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [LE R] [AddCommMonoid R] [One R] {M : Type v} (weights : M →₀ R) (nonneg : 0 ≤ weights) (total : (weights.sum fun x r => r) = 1) : Convexity.StdSimplex R M
Convexity.StdSimplex.ext 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M} : f.weights = g.weights → f = g
Convexity.iConvexComb_assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R J) (g : J → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) g) = Convexity.iConvexComb (Convexity.iConvexComb s f) g
Convexity.iConvexComb_comm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_9} {M : Type u_10} {I : Type u_11} {J : Type u_12} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R I) (g : Convexity.StdSimplex R J) (e : I → J → M) : (Convexity.iConvexComb f fun i => Convexity.iConvexComb g (e i)) = Convexity.iConvexComb g fun j => Convexity.iConvexComb f fun i => e i j
Convexity.ConvexSpace.mk' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] (sConvexComb : Convexity.StdSimplex R M → M) (sConvexComb_single : ∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) (assoc : ∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)), sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb f.join) : Convexity.ConvexSpace R M
Convexity.StdSimplex.ext_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M} : f = g ↔ f.weights = g.weights
Convexity.StdSimplex.weights_inj 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {f g : Convexity.StdSimplex R M} : f.weights = g.weights ↔ f = g
Convexity.iConvexComb_congr 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {w : Convexity.StdSimplex R I} {f g : I → M} (hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i) : Convexity.iConvexComb w f = Convexity.iConvexComb w g
Convexity.sConvexComb_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : Convexity.sConvexComb (Convexity.sConvexComb f) = Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f)
Convexity.StdSimplex.map_duple 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M) (f : M → N) : Convexity.StdSimplex.map f (Convexity.StdSimplex.duple x y hs ht h) = Convexity.StdSimplex.duple (f x) (f y) hs ht h
Convexity.StdSimplex.map_comp' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} {P : Type u_11} [IsStrictOrderedRing R] (g₁ : M → N) (g₂ : N → P) : Convexity.StdSimplex.map (g₂ ∘ g₁) = Convexity.StdSimplex.map g₂ ∘ Convexity.StdSimplex.map g₁
Convexity.ConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_9} (sConvexComb : Convexity.StdSimplex R M → M) (single : ∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) (assoc : ∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)), sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb (Convexity.sConvexComb f)) : Convexity.ConvexSpace R M
Convexity.iConvexComb_assoc' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R J) (g : I → J → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) = Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => (i, x)) (f i)) (Function.uncurry g)
Convexity.iConvexComb_assoc'' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : I → Type u_9} (s : Convexity.StdSimplex R I) (f : (i : I) → Convexity.StdSimplex R (J i)) (g : (i : I) → J i → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) = Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => ⟨i, x⟩) (f i)) (Sigma.uncurry g)
Convexity.sConvexComb_map_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : I → M) (s : Convexity.StdSimplex R (Convexity.StdSimplex R I)) : Convexity.sConvexComb (Convexity.StdSimplex.map (fun s => Convexity.iConvexComb s f) s) = Convexity.iConvexComb (Convexity.sConvexComb s) f
Convexity.StdSimplex.range_toFun_comp_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [Fintype M] : (Set.range fun t => ⇑t.weights) = (⋂ i, {s | 0 ≤ s i}) ∩ {s | ∑ i, s i = 1}
Convexity.iConvexComb_convexCombPair_comm_left 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e x) m) = Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e) m
Convexity.iConvexComb_convexCombPair_comm_right 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h m (e x)) = Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb f e)
Convexity.convexCombPair_iConvexComb_left 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (g : Convexity.StdSimplex R J) (e : J → M) (m : M) : Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g e) m = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map e g) (Convexity.StdSimplex.single m))
Convexity.convexCombPair_iConvexComb_right 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M) (g : Convexity.StdSimplex R J) (e : J → M) : Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb g e) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m) (Convexity.StdSimplex.map e g))
Convexity.iConvexComb_convexCombPair_comm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (e₁ e₂ : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e₁ x) (e₂ x)) = Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e₁) (Convexity.iConvexComb f e₂)
Convexity.sConvexComb_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (w w' : Convexity.StdSimplex R M) : Convexity.sConvexComb (Convexity.convexCombPair s t hs ht hst w w') = Convexity.convexCombPair s t hs ht hst (Convexity.sConvexComb w) (Convexity.sConvexComb w')
Convexity.StdSimplex.map_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (s : Convexity.StdSimplex R (Convexity.StdSimplex R I)) (f : I → J) : Convexity.StdSimplex.map f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map (Convexity.StdSimplex.map f) s)
Convexity.map_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} {J : Type u_7} {K : Type u_8} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {f : J → K} (s : Convexity.StdSimplex R I) (g : I → Convexity.StdSimplex R J) : Convexity.StdSimplex.map f (Convexity.iConvexComb s g) = Convexity.iConvexComb s (Convexity.StdSimplex.map f ∘ g)
Convexity.StdSimplex.restrict 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) : Convexity.StdSimplex K X
Convexity.iConvexComb_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : I → R) (hs : ∀ (i : I), 0 ≤ s i) (ht : ∀ (i : I), 0 ≤ t i) (h : ∀ (i : I), s i + t i = 1) (f : Convexity.StdSimplex R I) (m₁ m₂ : I → M) : (Convexity.iConvexComb f fun i => Convexity.convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) = Convexity.sConvexComb (Convexity.iConvexComb f fun i => Convexity.StdSimplex.duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)
Convexity.convexCombPair_iConvexComb_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {J₁ : Type u₁} {J₂ : Type u₂} (g₁ : Convexity.StdSimplex R J₁) (g₂ : Convexity.StdSimplex R J₂) (m₁ : J₁ → M) (m₂ : J₂ → M) : Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g₁ m₁) (Convexity.iConvexComb g₂ m₂) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map m₁ g₁) (Convexity.StdSimplex.map m₂ g₂))
Convexity.StdSimplex.mem_range_map_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} {N : Type u_10} [IsStrictOrderedRing R] (f : M → N) (s : Convexity.StdSimplex R N) : s ∈ Set.range (Convexity.StdSimplex.map f) ↔ ∀ x ∉ Set.range f, s.weights x = 0
Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h (Convexity.convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.duple m₁ m₂ hs' ht' h') (Convexity.StdSimplex.single m₃))
Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h m₁ (Convexity.convexCombPair s' t' hs' ht' h' m₂ m₃) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m₁) (Convexity.StdSimplex.duple m₂ m₃ hs' ht' h'))
Convexity.StdSimplex.restrict_singleton 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [IsDomain K] (w : Convexity.StdSimplex K X) (x : X) (hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0) : w.restrict {x} hx = Convexity.StdSimplex.single x
Convexity.StdSimplex.total_fin_two 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] (w : Convexity.StdSimplex R (Fin 2)) : w.weights 0 + w.weights 1 = 1
Convexity.StdSimplex.mk_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (x : M) {nonneg : 0 ≤ fun₀ | x => 1} {total : ((fun₀ | x => 1).sum fun x r => r) = 1} : { weights := fun₀ | x => 1, nonneg := nonneg, total := total } = Convexity.StdSimplex.single x
Convexity.StdSimplex.weights_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (w : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R I) : (Convexity.iConvexComb w f).weights = w.weights.sum fun i r => r • (f i).weights
Convexity.StdSimplex.support_weights_restrict 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] [IsDomain K] (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [DecidablePred fun x => x ∈ s] : (w.restrict s hs).weights.support = {x ∈ w.weights.support | x ∈ s}
Convexity.StdSimplex.weights_join 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u} [PartialOrder R] [Semiring R] {M : Type u_9} [IsStrictOrderedRing R] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : f.join.weights = f.weights.sum fun d r => r • d.weights
Convexity.StdSimplex.weights_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (f : Convexity.StdSimplex R (Convexity.StdSimplex R I)) : (Convexity.sConvexComb f).weights = f.weights.sum fun d r => r • d.weights
Convexity.StdSimplex.equivIcc_single_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : Convexity.StdSimplex.equivIcc (Convexity.StdSimplex.single 1) = 1
Convexity.StdSimplex.equivIcc_single_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : Convexity.StdSimplex.equivIcc (Convexity.StdSimplex.single 0) = 0
Convexity.StdSimplex.equivIcc_apply_coe 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] (s : Convexity.StdSimplex R' (Fin 2)) : ↑(Convexity.StdSimplex.equivIcc s) = s.weights 1
Convexity.StdSimplex.equivIcc_symm_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : Convexity.StdSimplex.equivIcc.symm 1 = Convexity.StdSimplex.single 1
Convexity.StdSimplex.equivIcc_symm_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] : Convexity.StdSimplex.equivIcc.symm 0 = Convexity.StdSimplex.single 0
Convexity.StdSimplex.weights_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (w w' : Convexity.StdSimplex R I) (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) : (Convexity.convexCombPair s t hs ht hst w w').weights = s • w.weights + t • w'.weights
Convexity.StdSimplex.weights_restrict 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{X : Type u_2} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : Convexity.StdSimplex K X) (s : Set X) (hs : ∃ x ∈ s, w.weights x ≠ 0) [DecidablePred fun x => x ∈ s] : (w.restrict s hs).weights = ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k)⁻¹ • Finsupp.filter (fun x => x ∈ s) w.weights
Convexity.StdSimplex.equivIcc_symm_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{R' : Type u_12} [Ring R'] [PartialOrder R'] [IsStrictOrderedRing R'] (t : ↑(Set.Icc 0 1)) : Convexity.StdSimplex.equivIcc.symm t = Convexity.StdSimplex.duple 0 1 ⋯ ⋯ ⋯
Convexity.StdSimplex.convexCombPair_restrict_restrict_compl 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
{I : Type u_6} {K : Type u_8} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (w : Convexity.StdSimplex K I) (s : Set I) (hs : ∃ x ∈ s, w.weights x ≠ 0) (hs' : ∃ x ∈ sᶜ, w.weights x ≠ 0) [DecidablePred fun x => x ∈ s] : Convexity.convexCombPair ((Finsupp.filter (fun x => x ∈ s) w.weights).sum fun _x k => k) ((Finsupp.filter (fun x => x ∉ s) w.weights).sum fun _x k => k) ⋯ ⋯ ⋯ (w.restrict s hs) (w.restrict sᶜ hs') = w
Convexity.StdSimplex.barycenter 📋 Mathlib.Geometry.Convex.ConvexSpace.Barycenter
{K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] [Nonempty M] [Fintype M] : Convexity.StdSimplex K M
Convexity.StdSimplex.subBarycenter 📋 Mathlib.Geometry.Convex.ConvexSpace.Barycenter
{K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (S : Finset M) (hS : S.Nonempty) : Convexity.StdSimplex K M
Convexity.StdSimplex.subBarycenter_singleton 📋 Mathlib.Geometry.Convex.ConvexSpace.Barycenter
{K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] (m : M) : Convexity.StdSimplex.subBarycenter {m} ⋯ = Convexity.StdSimplex.single m
Convexity.StdSimplex.barycenter_of_unique 📋 Mathlib.Geometry.Convex.ConvexSpace.Barycenter
{K : Type u_1} {M : Type u_2} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] [Unique M] : Convexity.StdSimplex.barycenter = Convexity.StdSimplex.single default
Convexity.StdSimplex.barycenter_fin_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Barycenter
{K : Type u_1} [Field K] [CharZero K] [LinearOrder K] [IsStrictOrderedRing K] : Convexity.StdSimplex.barycenter = Convexity.StdSimplex.single 0
Convexity.StdSimplex.topologicalSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] (M : Type v) : TopologicalSpace (Convexity.StdSimplex R M)
Convexity.StdSimplex.continuous_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} {N : Type v} (f : M → N) : Continuous (Convexity.StdSimplex.map f)
Convexity.StdSimplex.continuous_weights_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} (m : M) : Continuous fun t => t.weights m
Convexity.StdSimplex.isEmbedding_toFun_comp_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] (M : Type u_1) [Finite M] : Topology.IsEmbedding fun t => ⇑t.weights
Convexity.StdSimplex.isClosedEmbedding_toFun_comp_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] [OrderClosedTopology R] (M : Type u_1) [Finite M] : Topology.IsClosedEmbedding fun t => ⇑t.weights
Convexity.StdSimplex.continuous_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
{R : Type u} [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type v} {T : Type u_1} [TopologicalSpace T] (f : Convexity.StdSimplex R M → T) : Continuous f ↔ ∀ (ι : Type v) [Finite ι] (g : ι → M), Continuous (f ∘ Convexity.StdSimplex.map g)
Convexity.StdSimplex.continuous_iff' 📋 Mathlib.Geometry.Convex.ConvexSpace.Topology
(R : Type u) [PartialOrder R] [Ring R] [TopologicalSpace R] [IsStrictOrderedRing R] [IsTopologicalRing R] {M : Type u_1} {T : Type u_2} [TopologicalSpace T] (f : Convexity.StdSimplex R M → T) : Continuous f ↔ ∀ (s : Finset M), Continuous (f ∘ Convexity.StdSimplex.map Subtype.val)
Convexity.StdSimplex.compactSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(R : Type u_1) (M : Type u_2) [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [PartialOrder R] [IsStrictOrderedRing R] [CompactIccSpace R] [OrderClosedTopology R] [Finite M] : CompactSpace (Convexity.StdSimplex R M)
Convexity.StdSimplex.isBounded_range_toFun_comp_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(M : Type u_1) [Finite M] : Bornology.IsBounded (Set.range fun t => ⇑t.weights)
Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(M : Type u_1) [Fintype M] : Metric.diam (Set.range fun t => ⇑t.weights) ≤ 1
Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_one 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(M : Type u_1) [Fintype M] [Nontrivial M] : Metric.diam (Set.range fun t => ⇑t.weights) = 1
Convexity.StdSimplex.diam_range_toFun_comp_weights_subset_closedBall_eq_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(M : Type u_1) [Fintype M] [Subsingleton M] : Metric.diam (Set.range fun t => ⇑t.weights) = 0
Convexity.StdSimplex.range_toFun_comp_weights_subset_closedBall 📋 Mathlib.Geometry.Convex.ConvexSpace.CompactSpaceStdSimplex
(M : Type u_1) [Fintype M] : (Set.range fun t => ⇑t.weights) ⊆ Metric.closedBall 0 1
Convexity.StdSimplex.pathConnectedSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
(M : Type u_1) [Nonempty M] : PathConnectedSpace (Convexity.StdSimplex ℝ M)
Convexity.StdSimplex.homeomorphI 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
: Convexity.StdSimplex ℝ (Fin 2) ≃ₜ ↑unitInterval
Convexity.StdSimplex.continuous_duple 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
{M : Type u_1} (x y : M) : Continuous fun t => Convexity.StdSimplex.duple x y ⋯ ⋯ ⋯
Convexity.StdSimplex.continuous_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
{M : Type u_1} (x y : Convexity.StdSimplex ℝ M) : Continuous fun t => Convexity.convexCombPair ↑(unitInterval.symm t) ↑t ⋯ ⋯ ⋯ x y
Convexity.StdSimplex.homeomorphI_single_one 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
: Convexity.StdSimplex.homeomorphI (Convexity.StdSimplex.single 1) = 1
Convexity.StdSimplex.homeomorphI_single_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
: Convexity.StdSimplex.homeomorphI (Convexity.StdSimplex.single 0) = 0
Convexity.StdSimplex.homeomorphI_symm_one 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
: Convexity.StdSimplex.homeomorphI.symm 1 = Convexity.StdSimplex.single 1
Convexity.StdSimplex.homeomorphI_symm_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
: Convexity.StdSimplex.homeomorphI.symm 0 = Convexity.StdSimplex.single 0
Convexity.StdSimplex.homeomorphI_apply_coe 📋 Mathlib.Geometry.Convex.ConvexSpace.PathConnectedSpaceStdSimplex
(s : Convexity.StdSimplex ℝ (Fin 2)) : ↑(Convexity.StdSimplex.homeomorphI s) = s.weights 1
Pi.sConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R ((i : ι) → X i)) (i : ι) : Convexity.sConvexComb w i = Convexity.iConvexComb w fun x => x i
Prod.fst_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).1 = Convexity.iConvexComb w Prod.fst
Prod.snd_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).2 = Convexity.iConvexComb w Prod.snd
Pi.iConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R I) (f : I → (i : ι) → X i) (i : ι) : Convexity.iConvexComb w f i = Convexity.iConvexComb w fun j => f j i
Prod.fst_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).1 = Convexity.iConvexComb w fun i => (f i).1
Prod.snd_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).2 = Convexity.iConvexComb w fun i => (f i).2
Finsupp.iConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R I) (f : I → ι →₀ X) (i : ι) : (Convexity.iConvexComb w f) i = Convexity.iConvexComb w fun j => (f j) i
Finsupp.sConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
{R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R (ι →₀ X)) (i : ι) : (Convexity.sConvexComb w) i = Convexity.iConvexComb w fun x => x i
Convexity.subtypeVal_sConvexComb 📋 Mathlib.Geometry.Convex.Set
{R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (w : Convexity.StdSimplex R ↑s) : ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
Convexity.subtypeVal_iConvexComb 📋 Mathlib.Geometry.Convex.Set
{I : Type u_2} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (w : Convexity.StdSimplex R I) (f : I → ↑s) : ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
Convexity.IsConvexSet.of_sConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
{R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} (hs : ∀ (w : Convexity.StdSimplex R X), ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s) : Convexity.IsConvexSet R s
Convexity.IsConvexSet.sConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
{R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {w : Convexity.StdSimplex R X} {s : Set X} (hs : Convexity.IsConvexSet R s) (hw : ↑w.weights.support ⊆ s) : Convexity.sConvexComb w ∈ s
Convexity.IsConvexSet.iConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
{ι : Type u_1} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} (hs : Convexity.IsConvexSet R s) {w : Convexity.StdSimplex R ι} {f : ι → X} (hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s) : Convexity.iConvexComb w f ∈ s
Convexity.StdSimplex.affineMapMk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {X : Type u_3} [Convexity.ConvexSpace R X] (f : M → X) : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) X
Convexity.StdSimplex.affineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} (f : M → N) : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) (Convexity.StdSimplex R N)
Convexity.StdSimplex.affineMapMk_surjective 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (s : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y) : ∃ f, Convexity.StdSimplex.affineMapMk f = s
Convexity.StdSimplex.affineMap_id 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (M : Type u_2) : Convexity.StdSimplex.affineMap id = Convexity.ConvexSpace.AffineMap.id (Convexity.StdSimplex R M)
Convexity.StdSimplex.affineMapMk_single 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (f : M → Y) (m : M) : (Convexity.StdSimplex.affineMapMk f) (Convexity.StdSimplex.single m) = f m
Convexity.StdSimplex.comp_affineMapMk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} {Z : Type u_4} [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] (f : Convexity.ConvexSpace.AffineMap R Y Z) (g : M → Y) : f.comp (Convexity.StdSimplex.affineMapMk g) = Convexity.StdSimplex.affineMapMk (⇑f ∘ g)
Convexity.StdSimplex.affineMapMk_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (f : M → Y) (s : Convexity.StdSimplex R M) : (Convexity.StdSimplex.affineMapMk f) s = Convexity.iConvexComb s f
Convexity.StdSimplex.coe_affineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {N : Type u_3} (f : M → N) : ⇑(Convexity.StdSimplex.affineMap f) = Convexity.StdSimplex.map f
Convexity.StdSimplex.affineMap_ext 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y} (h : ∀ (i : M), f (Convexity.StdSimplex.single i) = g (Convexity.StdSimplex.single i)) : f = g
Convexity.StdSimplex.affineMap_ext_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
{R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y} : f = g ↔ ∀ (i : M), f (Convexity.StdSimplex.single i) = g (Convexity.StdSimplex.single i)
Convexity.StdSimplex.isAffineMap_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
(R : Type u_2) (I : Type u_5) [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Convexity.IsAffineMap R Convexity.StdSimplex.weights
convexCombination_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommMonoid M} {inst✝⁴ : Module R M} {inst✝⁵ : Convexity.ConvexSpace R M} [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.sConvexComb w = w.weights.sum fun m r => r • m
Convexity.IsModuleConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] (sConvexComb_eq_sum : ∀ (w : Convexity.StdSimplex R M), Convexity.sConvexComb w = w.weights.sum fun m r => r • m) : Convexity.IsModuleConvexSpace R M
Convexity.IsModuleConvexSpace.sConvexComb_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommMonoid M} {inst✝⁴ : Module R M} {inst✝⁵ : Convexity.ConvexSpace R M} [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.sConvexComb w = w.weights.sum fun m r => r • m
Convexity.iConvexComb_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M) : Convexity.iConvexComb w f = w.weights.sum fun i r => r • f i
Convexity.subtypeVal_submodule_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{F : Type u_1} {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R I) (f : I → ↥S) : ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
Convexity.subtypeVal_submodule_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R ↥S) : ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
Convexity.IsAffineMap.map_sum_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {N : Type u_4} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M → N} [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] (hf : Convexity.IsAffineMap R f) (w : Convexity.StdSimplex R I) (g : I → M) : f (w.weights.sum fun i r => r • g i) = w.weights.sum fun i r => r • f (g i)
Convexity.StdSimplex.affineMapMk_apply_eq_sum_of_fintype 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Fintype I] (f : I → M) (w : Convexity.StdSimplex R I) : (Convexity.StdSimplex.affineMapMk f) w = ∑ i, w.weights i • f i
Convexity.StdSimplex.coe_affineMapMk_of_fintype 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
{R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Fintype I] (f : I → M) : ⇑(Convexity.StdSimplex.affineMapMk f) = fun w => ∑ i, w.weights i • f i
Set.convexHull_eq_range_iConvexComb 📋 Mathlib.Analysis.Convex.StdSimplex
{R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) : (convexHull R) s = Set.range ⇑(Convexity.StdSimplex.affineMapMk fun x => ↑x)
Set.Finite.convexHull_eq_image 📋 Mathlib.Analysis.Convex.StdSimplex
{R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) : (convexHull R) s = Set.range ⇑(Convexity.StdSimplex.affineMapMk fun x => ↑x)
Convexity.StdSimplex.continuous_of_isAffineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.ModuleTopology
{R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [Convexity.IsModuleConvexSpace R E] (f : Convexity.StdSimplex R ι → E) (hf : Convexity.IsAffineMap R f) : Continuous f
Convexity.StdSimplex.continuous_of_affineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.ModuleTopology
{R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [Convexity.IsModuleConvexSpace R E] (f : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R ι) E) : Continuous ⇑f
SimplexCategory.toTop₀_obj 📋 Mathlib.AlgebraicTopology.TopologicalSimplex
(n : SimplexCategory) : SimplexCategory.toTop₀.obj n = TopCat.of (Convexity.StdSimplex ℝ (Fin (n.len + 1)))
SimplexCategory.toTop_obj 📋 Mathlib.AlgebraicTopology.TopologicalSimplex
(X : SimplexCategory) : SimplexCategory.toTop.{u}.obj X = TopCat.uliftFunctor.obj (TopCat.of (Convexity.StdSimplex ℝ (Fin (X.len + 1))))
SimplexCategory.toTop₀_map 📋 Mathlib.AlgebraicTopology.TopologicalSimplex
{X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : SimplexCategory.toTop₀.map f = TopCat.ofHom { toFun := Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ }
SimplexCategory.toTop_map 📋 Mathlib.AlgebraicTopology.TopologicalSimplex
{X✝ Y✝ : SimplexCategory} (f : X✝ ⟶ Y✝) : SimplexCategory.toTop.{u}.map f = TopCat.uliftFunctor.map (TopCat.ofHom { toFun := Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })
TopCat.toSSetObjEquiv 📋 Mathlib.AlgebraicTopology.SingularSet
(X : TopCat) (n : SimplexCategoryᵒᵖ) : (TopCat.toSSet.obj X).obj n ≃ C(Convexity.StdSimplex ℝ (Fin ((Opposite.unop n).len + 1)), ↑X)
SSet.stdSimplexToTop_app_app_hom_apply_down_hom_apply 📋 Mathlib.AlgebraicTopology.SingularSet
(X : SimplexCategory) (X✝ : SimplexCategoryᵒᵖ) (a✝ : (SSet.stdSimplex.obj X).obj X✝) (a✝¹ : ↑(Opposite.unop (SimplexCategory.toTop.{u}.op.obj X✝))) : (TopCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplexToTop.app X).app X✝)) a✝).down) a✝¹ = (SSet.toTopSimplex.hom.app X).hom' ((((sSetTopAdj.unit.app (SSet.stdSimplex.obj X)).app X✝).hom' a✝).down.hom' a✝¹)
instUniqueStdSimplexRealFinHAddNatLenMkOfNat 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: Unique (Convexity.StdSimplex ℝ (Fin ({ len := 0 }.len + 1)))
TopCat.stdSimplexHomeomorphI 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: Convexity.StdSimplex ℝ (Fin 2) ≃ₜ ↑TopCat.I
SimplexCategory.toTopHomeo 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
(n : SimplexCategory) : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) ≃ₜ Convexity.StdSimplex ℝ (Fin (n.len + 1))
TopCat.stdSimplexHomeomorphI_vertex_one 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: TopCat.stdSimplexHomeomorphI (Convexity.StdSimplex.single 1) = 1
TopCat.stdSimplexHomeomorphI_vertex_zero 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: TopCat.stdSimplexHomeomorphI (Convexity.StdSimplex.single 0) = 0
TopCat.stdSimplexHomeomorphI_symm_one 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: TopCat.stdSimplexHomeomorphI.symm 1 = Convexity.StdSimplex.single 1
TopCat.stdSimplexHomeomorphI_symm_zero 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
: TopCat.stdSimplexHomeomorphI.symm 0 = Convexity.StdSimplex.single 0
TopCat.toSSetObj₀Equiv_symm_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} (a✝ : ↑X) : TopCat.toSSetObj₀Equiv.symm a✝ = (X.toSSetObjEquiv (Opposite.op { len := 0 })).symm { toFun := fun x => a✝, continuous_toFun := ⋯ }
TopCat.toSSetObj₀Equiv_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} (a✝ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) : TopCat.toSSetObj₀Equiv a✝ = ((X.toSSetObjEquiv (Opposite.op { len := 0 })) a✝) default
SimplexCategory.toTopHomeo_naturality_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{n m : SimplexCategory} (f : n ⟶ m) (x : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n))) : m.toTopHomeo ((CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) x) = Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) (n.toTopHomeo x)
TopCat.toSSetObjEquiv_σ_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} {n : ℕ} (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (i : Fin (n + 1)) (z : Convexity.StdSimplex ℝ (Fin (n + 2))) : ((X.toSSetObjEquiv (Opposite.op { len := n + 1 })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj X) i)) x)) z = ((X.toSSetObjEquiv (Opposite.op { len := n })) x) (Convexity.StdSimplex.map i.predAbove z)
SimplexCategory.toTopHomeo_naturality 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{n m : SimplexCategory} (f : n ⟶ m) : ⇑m.toTopHomeo ∘ ⇑(CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) = Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) ∘ ⇑n.toTopHomeo
TopCat.toSSetObjEquiv_δ_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} {n : ℕ} (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n + 1 })) (i : Fin (n + 2)) (z : Convexity.StdSimplex ℝ (Fin (n + 1))) : ((X.toSSetObjEquiv (Opposite.op { len := n })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) i)) x)) z = ((X.toSSetObjEquiv (Opposite.op { len := n + 1 })) x) (Convexity.StdSimplex.map i.succAbove z)
SimplexCategory.toTopHomeo_symm_naturality_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{n m : SimplexCategory} (f : n ⟶ m) (x : Convexity.StdSimplex ℝ (Fin (n.len + 1))) : m.toTopHomeo.symm (Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) x) = (CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) (n.toTopHomeo.symm x)
TopCat.toSSetObjEquiv_naturality_apply 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (x : (TopCat.toSSet.obj X).obj (Opposite.op m)) (z : Convexity.StdSimplex ℝ (Fin (n.len + 1))) : ((X.toSSetObjEquiv (Opposite.op n)) ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) x)) z = ((X.toSSetObjEquiv (Opposite.op m)) x) (Convexity.StdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) z)
TopCat.toSSetObjEquiv_symm_naturality 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{X : TopCat} {n m : SimplexCategory} (f : n ⟶ m) (g : C(Convexity.StdSimplex ℝ (Fin (m.len + 1)), ↑X)) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.obj X).map f.op)) ((X.toSSetObjEquiv (Opposite.op m)).symm g) = (X.toSSetObjEquiv (Opposite.op n)).symm (g.comp { toFun := Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f), continuous_toFun := ⋯ })
SimplexCategory.toTopHomeo_symm_naturality 📋 Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
{n m : SimplexCategory} (f : n ⟶ m) : ⇑m.toTopHomeo.symm ∘ Convexity.StdSimplex.map ⇑(CategoryTheory.ConcreteCategory.hom f) = ⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) ∘ ⇑n.toTopHomeo.symm
AddTorsor.convexCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [AddCommGroup V] [Module R V] [AddTorsor V P] (s : Convexity.StdSimplex R P) : P
Convexity.IsAffineConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] (sConvexComb_eq_convexComb : ∀ (w : Convexity.StdSimplex R P), Convexity.sConvexComb w = AddTorsor.convexCombination w) : Convexity.IsAffineConvexSpace R V P
Convexity.IsAffineConvexSpace.sConvexComb_eq_convexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} {inst✝ : Ring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommGroup V} {inst✝⁴ : Module R V} {inst✝⁵ : AddTorsor V P} {inst✝⁶ : Convexity.ConvexSpace R P} [self : Convexity.IsAffineConvexSpace R V P] (w : Convexity.StdSimplex R P) : Convexity.sConvexComb w = AddTorsor.convexCombination w
AddTorsor.convexCombination_assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] (f : Convexity.StdSimplex R (Convexity.StdSimplex R P)) : AddTorsor.convexCombination (Convexity.StdSimplex.map AddTorsor.convexCombination f) = AddTorsor.convexCombination f.join
AddTorsor.convexCombination_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
AddTorsor.sConvexComb_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
AddTorsor.iConvexComb_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
{R : Type u_1} {V : Type u_2} {P : Type u_3} {I : Type u_4} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R I) (f : I → P) : Convexity.iConvexComb s f = (Finset.affineCombination R s.weights.support f) ⇑s.weights
Convexity.dist_sConvexComb_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (x : X) (f : Convexity.StdSimplex ℝ X) : dist x (Convexity.sConvexComb f) ≤ Convexity.iConvexComb f (dist x)
Convexity.dist_sConvexComb_left_le 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ X) (x : X) : dist (Convexity.sConvexComb f) x ≤ Convexity.iConvexComb f fun x_1 => dist x_1 x
Convexity.dist_iConvexComb_left_le 📋 Mathlib.Analysis.Convex.MetricSpace
{I : Type u_1} {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ I) (g : I → X) (x : X) : dist (Convexity.iConvexComb f g) x ≤ Convexity.iConvexComb f fun i => dist (g i) x
Convexity.dist_iConvexComb_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
{I : Type u_1} {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (x : X) (f : Convexity.StdSimplex ℝ I) (g : I → X) : dist x (Convexity.iConvexComb f g) ≤ Convexity.iConvexComb f fun i => dist x (g i)
Convexity.dist_convexCombination_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3} (f : Convexity.StdSimplex ℝ ι) (x y : ι → X) : dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
Convexity.dist_iConvexComb_le 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3} (f : Convexity.StdSimplex ℝ ι) (x y : ι → X) : dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] [self : Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ (X × X)) : dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤ Convexity.iConvexComb f fun x => dist x.1 x.2
Convexity.IsConvexDist.mk 📋 Mathlib.Analysis.Convex.MetricSpace
{X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] (dist_iConvexComb_fst_snd_le : ∀ (f : Convexity.StdSimplex ℝ (X × X)), dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤ Convexity.iConvexComb f fun x => dist x.1 x.2) : Convexity.IsConvexDist X

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c