mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : SetLike F M
inst✝¹ : AddSubmonoidClass F M
inst✝ : SMulMemClass F R M
f g : M → N
⊢ ∀ (x : M), ((StdSimplex.single x).weights.sum fun m r ↦ r • m) = x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝⁹ : Semiring R
inst✝⁸ : PartialOrder R
inst✝⁷ : IsStrictOrderedRing R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : SetLike F M
inst✝¹ : AddSubmonoidClass F M
inst✝ : SMulMemClass F R M
f g : M → N
⊢ ∀ (f : StdSimplex R (StdSimplex R M)),
    ((StdSimplex.map (fun w ↦ w.weights.sum fun m r ↦ r • m) f).weights.sum fun m r ↦ r • m) =
      f.join.weights.sum fun m r ↦ r • m

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
I : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
w : StdSimplex R I
f : I → M
⊢ iConvexComb w f = w.weights.sum fun i r ↦ r • f i

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: 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✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : M
⊢ convexCombPair a b ha hb hab x y = a • x + b • y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
f : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
hf : IsAffineMap R f
w : 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)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
f : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
a b : R
hf : IsAffineMap R f
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x y : M
⊢ f (a • x + b • y) = a • f x + b • f y

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
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✝⁴ : SetLike F M
inst✝³ : AddSubmonoidClass F M
inst✝² : SMulMemClass F R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
S : F
w : StdSimplex R M
hw : ↑w.weights.support ⊆ ↑S
m : M
hm : w.weights m ≠ 0
⊢ m ∈ ↑w.weights.support

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
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✝⁴ : SetLike F M
inst✝³ : AddSubmonoidClass F M
inst✝² : SMulMemClass F R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
S : F
⊢ IsConvexSet R ↑S

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
S : F
w : StdSimplex R ↥S
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
w : StdSimplex R (M × N)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M✝ : Type u_3
N : Type u_4
I : Type u_5
inst✝¹⁷ : Semiring R
inst✝¹⁶ : PartialOrder R
inst✝¹⁵ : IsStrictOrderedRing R
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R M✝
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : SetLike F M✝
inst✝⁹ : AddSubmonoidClass F M✝
inst✝⁸ : SMulMemClass F R M✝
f g : M✝ → N
inst✝⁷ : ConvexSpace R M✝
inst✝⁶ : IsModuleConvexSpace R M✝
inst✝⁵ : ConvexSpace R N
inst✝⁴ : IsModuleConvexSpace R N
x y : M✝
s t : Set M✝
a b : R
ι : Type u_6
M : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → ConvexSpace R (M i)
inst✝ : ∀ (i : ι), IsModuleConvexSpace R (M i)
w : StdSimplex R ((i : ι) → M i)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
⊢ t ∈ f ⁻¹' {0}ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: F : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
I : Type u_5
inst✝¹³ : Semiring R
inst✝¹² : PartialOrder R
inst✝¹¹ : IsStrictOrderedRing R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R N
inst✝⁶ : SetLike F M
inst✝⁵ : AddSubmonoidClass F M
inst✝⁴ : SMulMemClass F R M
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
x y : M
s t : Set M
a b : R
ι : Type u_6
w : StdSimplex R (ι →₀ M)
⊢ sConvexComb w = w.weights.sum fun m r ↦ r • m

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
f g : M → N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
hf : IsAffineMap R f
hg : IsAffineMap R g
w : StdSimplex R M
⊢ (f + g) (sConvexComb w) = sConvexComb (StdSimplex.map (f + g) w)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
n k : ℕ
h_card : finrank 𝕜 E + 1 ≤ k
hk :
  ∀ {ι : Type u_1} {F : ι → Set E} {s : Finset ι},
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → #s = k → (⋂ i ∈ s, F i).Nonempty
ι : Type u_1
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
hn : #s = k + 1
a : ↥s → E := fun i ↦ ⋯.some
h_ind : ¬AffineIndependent 𝕜 a
I : Set ↥s
p : E
hp_I : p ∈ (convexHull 𝕜) (a '' I)
hp_Ic : p ∈ (convexHull 𝕜) (a '' Iᶜ)
i : ↥s
this : ∀ (J : Set ↥s), i ∈ J → (convexHull 𝕜) (a '' Jᶜ) ⊆ F ↑i
⊢ p ∈ F ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: 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✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsAffineMap R fun x ↦ x.1 + x.2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: 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✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x + y) (s + t)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
I : Type u_5
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsStrictOrderedRing R
s : StdSimplex R (StdSimplex R I)
⊢ (sConvexComb s).weights = sConvexComb (map weights s)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
f : M → N
hf : IsAffineMap R f
w : StdSimplex R M
⊢ (-f) (sConvexComb w) = sConvexComb (StdSimplex.map (-f) w)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Semiring R
inst✝⁹ : PartialOrder R
inst✝⁸ : IsStrictOrderedRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : ConvexSpace R M
inst✝² : IsModuleConvexSpace R M
inst✝¹ : ConvexSpace R N
inst✝ : IsModuleConvexSpace R N
f g : M → N
hf : IsAffineMap R f
hg : IsAffineMap R g
⊢ IsAffineMap R (f - g)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht✝ : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ 0 ≤ 1 - f j

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsAffineMap R Neg.neg

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x : M
s : Set M
hs : IsStarConvexSet R x s
⊢ IsStarConvexSet R (-x) (-s)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsAffineMap R fun x ↦ x.1 - x.2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Convex.ConvexSpace.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsStrictOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : ConvexSpace R M
inst✝ : IsModuleConvexSpace R M
x y : M
s t : Set M
hs : IsStarConvexSet R x s
ht : IsStarConvexSet R y t
⊢ IsStarConvexSet R (x - y) (s - t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
h : ∅ ∈ K.faces
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x : E
⊢ x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ (convexHull 𝕜) ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ (convexHull 𝕜) ↑s ⊆ K.space

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
hs : s ∈ K.faces
ht : t ∈ K.faces
⊢ Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨
    ∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val
down_closed : IsLowerSet faces
inter_subset_convexHull : ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)
⊢ faces \ {∅} = {f | f ∈ faces ∧ f.Nonempty}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
faces : Set (Finset E)
indep : ∀ s ∈ faces, AffineIndependent 𝕜 Subtype.val
down_closed : IsLowerSet faces
inter_subset_convexHull : ∀ s ∈ faces, ∀ t ∈ faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)
⊢ IsRelLowerSet (faces \ {∅}) Finset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
⊢ K.vertices = ⋃ k ∈ K.faces, ↑k

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
h : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ (convexHull 𝕜) ↑{x}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
x : E
hx : x ∈ K.vertices
hs : s ∈ K.faces
⊢ x ∈ (convexHull 𝕜) ↑s ↔ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : Ring 𝕜
inst✝² : PartialOrder 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s : Finset E
hs : s ∈ K.faces
⊢ s ∉ K.facets ↔ ∃ t ∈ K.faces, s ⊂ t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: X : Type u_2
inst✝³ : ConvexSpace ℝ X
inst✝² : MetricSpace X
inst✝¹ : IsConvexDist X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
⊢ Continuous fun i ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : ι → Set E
s : Finset ι
h_card : finrank 𝕜 E + 1 ≤ #s
h_convex : ∀ i ∈ s, Convex 𝕜 (F i)
h_inter : ∀ I ⊆ s, #I = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
⊢ (⋂ i ∈ s, F i).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁴ : ConvexSpace ℝ X
inst✝³ : MetricSpace X
inst✝² : IsConvexDist X
inst✝¹ : BoundedSpace X
T : Type u_3
inst✝ : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
i : T
⊢ 0 ≤ 1 - f i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := ⋯.some
this : ‖f.weights.sum fun a b ↦ b • (a.1 -ᵥ a.2)‖ ≤ f.weights.sum fun a b ↦ b * ‖a.1 -ᵥ a.2‖
⊢ dist (((f.weights.support.weightedVSubOfPoint Prod.fst p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p)
      (((f.weights.support.weightedVSubOfPoint Prod.snd p) fun i ↦ (fun x r ↦ r) i (f.weights i)) +ᵥ p) ≤
    iConvexComb f fun x ↦ dist x.1 x.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝⁶ : ConvexSpace ℝ X
inst✝⁵ : MetricSpace X
inst✝⁴ : IsConvexDist X
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤ iConvexComb f fun x ↦ dist x.1 x.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.MetricSpace

Goal state before:
pp: I : Type u_1
X : Type u_2
inst✝² : ConvexSpace ℝ X
inst✝¹ : MetricSpace X
inst✝ : IsConvexDist X
s : Set X
hs : IsConvexSet ℝ s
⊢ IsConvexDist ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left✝ : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
⊢ ↑I ⊆ ↑J

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
⊢ IsRelLowerSet ({s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet) Finset.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
G : SimpleGraph ι
⊢ ∀ (v : ι), {v} ∈ {s | ∃ v, s = {v}} ∪ Sym2.toFinset '' G.edgeSet

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
I : Finset (Set E)
hI_ss : I ⊆ F
hI_card : #I ≤ finrank 𝕜 E + 1
J : Finset (Set E)
left✝ : I ⊆ J
hJ_ss : J ⊆ F
hJ_card : #J = finrank 𝕜 E + 1
this : ⋂₀ ↑J ⊆ ⋂₀ ↑I
⊢ #J = finrank 𝕜 E + 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
F : Finset (Set E)
h_card : finrank 𝕜 E + 1 ≤ #F
h_convex : ∀ X ∈ F, Convex 𝕜 X
h_inter : ∀ G ⊆ F, #G = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
⊢ (⋂₀ ↑F).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: 𝕜 : Type ?u.4
E : Type ?u.12
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : DecidableEq E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
abstract : PreAbstractSimplicialComplex E
indep : AffineIndependent 𝕜 Subtype.val
s t : Finset E
hs : s ∈ abstract.faces
ht : t ∈ abstract.faces
⊢ (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.Radon

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : FiniteDimensional 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : T2Space E
F : ι → Set E
h_convex : ∀ (i : ι), Convex 𝕜 (F i)
h_compact : ∀ (i : ι), IsCompact (F i)
h_inter : ∀ (I : Finset ι), #I ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
h_nonempty : Nonempty ι
I : Finset ι
⊢ ∀ i ∈ I, Convex 𝕜 (F i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : DecidableEq 𝕜
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
abstract : PreAbstractSimplicialComplex ι
⊢ AffineIndependent 𝕜 Subtype.val

Tactic:
by

Goal state after: