[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
⊢ Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s
[PROOFSTEP]
rintro hA a b ha hb hab w ⟨au, bv, ⟨u, hu, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
hA : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hu : u ∈ s
v : E
hv : v ∈ s
⊢ (fun x x_1 => x + x_1) ((fun x => a • x) u) ((fun x => b • x) v) ∈ s
[PROOFSTEP]
exact hA hu hv ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
⊢ Convex 𝕜 (⋃ (i : ι), s i)
[PROOFSTEP]
rintro x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : x ∈ ⋃ (i : ι), s i
y : E
hy : y ∈ ⋃ (i : ι), s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ⋃ (i : ι), s i
[PROOFSTEP]
rw [mem_iUnion] at hx hy ⊢
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : ∃ i, x ∈ s i
y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ i, a • x + b • y ∈ s i
[PROOFSTEP]
obtain ⟨i, hx⟩ := hx
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
hy : ∃ i, y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ ∃ i, a • x + b • y ∈ s i
[PROOFSTEP]
obtain ⟨j, hy⟩ := hy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ ∃ i, a • x + b • y ∈ s i
[PROOFSTEP]
obtain ⟨k, hik, hjk⟩ := hdir i j
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s✝ : Set E
x✝ : E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun x x_1 => x ⊆ x_1) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ ∃ i, a • x + b • y ∈ s i
[PROOFSTEP]
exact ⟨k, hc (hik hx) (hjk hy) ha hb hab⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
c : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)
[PROOFSTEP]
rw [sUnion_eq_iUnion]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 F
s : Set E
x : E
c : Set (Set E)
hdir : DirectedOn (fun x x_1 => x ⊆ x_1) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ (i : ↑c), ↑i)
[PROOFSTEP]
exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
⊢ Convex 𝕜 s ↔ Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
[PROOFSTEP]
refine' convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h hx hy, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
⊢ (Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
    ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
[PROOFSTEP]
intro h x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ s
[PROOFSTEP]
obtain rfl | hxy := eq_or_ne x y
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hy : x ∈ s
⊢ a • x + b • x ∈ s
[PROOFSTEP]
rwa [Convex.combo_self hab]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
h : Set.Pairwise s fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxy : x ≠ y
⊢ a • x + b • y ∈ s
[PROOFSTEP]
exact h hx hy hxy ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ x y : E
⊢ Convex 𝕜 [x-[𝕜]y]
[PROOFSTEP]
rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (ap • x + bp • y) + b • (aq • x + bq • y) ∈ [x-[𝕜]y]
[PROOFSTEP]
refine'
  ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
    add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
[PROOFSTEP]
rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
[PROOFSTEP]
simp_rw [add_smul, mul_smul, smul_add]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ap • x + b • aq • x + (a • bp • y + b • bq • y) = a • ap • x + a • bp • y + (b • aq • x + b • bq • y)
[PROOFSTEP]
exact add_add_add_comm _ _ _ _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (↑f '' s)
[PROOFSTEP]
intro x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : F
hx : x ∈ ↑f '' s
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f '' s
[PROOFSTEP]
obtain ⟨x', hx', rfl⟩ := mem_image_iff_bex.1 hx
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
y : F
hy : y ∈ ↑f '' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
⊢ a • ↑f x' + b • y ∈ ↑f '' s
[PROOFSTEP]
obtain ⟨y', hy', rfl⟩ := mem_image_iff_bex.1 hy
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
y' : E
hy' : y' ∈ s
hy : ↑f y' ∈ ↑f '' s
⊢ a • ↑f x' + b • ↑f y' ∈ ↑f '' s
[PROOFSTEP]
exact ⟨a • x' + b • y', hs hx' hy' ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x' : E
hx' : x' ∈ s
hx : ↑f x' ∈ ↑f '' s
y' : E
hy' : y' ∈ s
hy : ↑f y' ∈ ↑f '' s
⊢ ↑f (a • x' + b • y') = a • ↑f x' + b • ↑f y'
[PROOFSTEP]
rw [f.map_add, f.map_smul, f.map_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
x : E
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
⊢ Convex 𝕜 (↑f ⁻¹' s)
[PROOFSTEP]
intro x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
x✝ : E
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑f ⁻¹' s
[PROOFSTEP]
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s✝ : Set E
x✝ : E
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : x ∈ ↑f ⁻¹' s
y : E
hy : y ∈ ↑f ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • ↑f x + b • ↑f y ∈ s
[PROOFSTEP]
exact hs hx hy ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)
[PROOFSTEP]
rw [← add_image_prod]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 ((fun x => x.fst + x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 (z +ᵥ s)
[PROOFSTEP]
simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ({z} + s)
[PROOFSTEP]
exact (convex_singleton _).add hs
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x => z + x) ⁻¹' s)
[PROOFSTEP]
intro x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s
[PROOFSTEP]
have h := hs hx hy ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x✝ : E
hs : Convex 𝕜 s
z x : E
hx : x ∈ (fun x => z + x) ⁻¹' s
y : E
hy : y ∈ (fun x => z + x) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ s
⊢ a • x + b • y ∈ (fun x => z + x) ⁻¹' s
[PROOFSTEP]
rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
x : E
hs : Convex 𝕜 s
z : E
⊢ Convex 𝕜 ((fun x => x + z) ⁻¹' s)
[PROOFSTEP]
simpa only [add_comm] using hs.translate_preimage_right z
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x : E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w = r}
[PROOFSTEP]
simp_rw [le_antisymm_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x : E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w ≤ r ∧ r ≤ f w}
[PROOFSTEP]
exact (convex_halfspace_le h r).inter (convex_halfspace_ge h r)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r : β
⊢ Convex 𝕜 (Iio r)
[PROOFSTEP]
intro x hx y hy a b ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r
[PROOFSTEP]
obtain rfl | ha' := ha.eq_or_lt
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : 0 + b = 1
⊢ 0 • x + b • y ∈ Iio r
[PROOFSTEP]
rw [zero_add] at hab 
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 0
hab : b = 1
⊢ 0 • x + b • y ∈ Iio r
[PROOFSTEP]
rwa [zero_smul, zero_add, hab, one_smul]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
[PROOFSTEP]
rw [mem_Iio] at hx hy 
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : AddCommMonoid E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
s : Set E
x✝ : E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
r x : β
hx : x < r
y : β
hy : y < r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
[PROOFSTEP]
calc
  a • x + b • y < a • r + b • r := add_lt_add_of_lt_of_le (smul_lt_smul_of_pos hx ha') (smul_le_smul_of_nonneg hy.le hb)
  _ = r := Convex.combo_self hab _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedCommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
hs : Convex 𝕜 s
z : E
c : 𝕜
⊢ Convex 𝕜 ((fun x => z + c • x) '' s)
[PROOFSTEP]
simpa only [← image_smul, ← image_vadd, image_image] using (hs.smul c).vadd z
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ Convex 𝕜 (openSegment 𝕜 a b)
[PROOFSTEP]
rw [convex_iff_openSegment_subset]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b : E
⊢ ∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
[PROOFSTEP]
rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ z ⟨a, b, ha, hb, hab, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (ap • a✝ + bp • b✝) + b • (aq • a✝ + bq • b✝) ∈ openSegment 𝕜 a✝ b✝
[PROOFSTEP]
refine' ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, _, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * ap + b * aq
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * bp + b * bq
[PROOFSTEP]
positivity
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
[PROOFSTEP]
rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : StrictOrderedCommSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a✝ b✝ : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a * ap + b * aq) • a✝ + (a * bp + b * bq) • b✝ = a • (ap • a✝ + bp • b✝) + b • (aq • a✝ + bq • b✝)
[PROOFSTEP]
simp_rw [add_smul, mul_smul, smul_add, add_add_add_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • y ∈ s
[PROOFSTEP]
have h : x + t • y = (1 - t) • x + t • (x + y) := by rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • y = (1 - t) • x + t • (x + y)
[PROOFSTEP]
rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ x + t • y ∈ s
[PROOFSTEP]
rw [h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s
[PROOFSTEP]
exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • x ∈ s
[PROOFSTEP]
simpa using hs.add_smul_mem zero_mem (by simpa using hx) ht
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ 0 + x ∈ s
[PROOFSTEP]
simpa using hx
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ MapsTo (↑(AffineMap.lineMap x y)) (Icc 0 1) s
[PROOFSTEP]
simpa only [mapsTo', segment_eq_image_lineMap] using h.segment_subset hx hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ x + t • (y - x) ∈ s
[PROOFSTEP]
rw [add_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t✝ : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : t ∈ Icc 0 1
⊢ t • (y - x) + x ∈ s
[PROOFSTEP]
exact h.lineMap_mem hx hy ht
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
Q : AffineSubspace 𝕜 E
⊢ Convex 𝕜 ↑Q
[PROOFSTEP]
intro x hx y hy a b _ _ hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
Q : AffineSubspace 𝕜 E
x : E
hx : x ∈ ↑Q
y : E
hy : y ∈ ↑Q
a b : 𝕜
a✝¹ : 0 ≤ a
a✝ : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ ↑Q
[PROOFSTEP]
rw [eq_sub_of_add_eq hab, ← AffineMap.lineMap_apply_module]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
Q : AffineSubspace 𝕜 E
x : E
hx : x ∈ ↑Q
y : E
hy : y ∈ ↑Q
a b : 𝕜
a✝¹ : 0 ≤ a
a✝ : 0 ≤ b
hab : a + b = 1
⊢ ↑(AffineMap.lineMap x y) b ∈ ↑Q
[PROOFSTEP]
exact AffineMap.lineMap_mem b hx hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
⊢ Convex 𝕜 (↑f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex 𝕜 (↑f x) (↑f '' s)
[PROOFSTEP]
exact (hs hx).affine_image _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s - t)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + -t)
[PROOFSTEP]
exact hs.add ht.neg
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s
[PROOFSTEP]
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s
[PROOFSTEP]
exact h.smul_mem_of_zero_mem zero_mem hx ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one ht⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
[PROOFSTEP]
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
[GOAL]
case inl.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ ∃ z, z ∈ s ∧ (0 + 0) • z = 0 • x + 0 • y
[PROOFSTEP]
use x, hx
[GOAL]
case right
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ (0 + 0) • x = 0 • x + 0 • y
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
[PROOFSTEP]
replace hpq : 0 < p + q := (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff' hp hq).1 hpq)
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
[PROOFSTEP]
refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
[PROOFSTEP]
simp only [smul_add, smul_smul, mul_div_cancel' _ hpq.ne']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
⊢ p • s + q • s ⊆ (p + q) • s
[PROOFSTEP]
rintro _ ⟨_, _, ⟨v₁, h₁, rfl⟩, ⟨v₂, h₂, rfl⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
v₁ : E
h₁ : v₁ ∈ s
v₂ : E
h₂ : v₂ ∈ s
⊢ (fun x x_1 => x + x_1) ((fun x => p • x) v₁) ((fun x => q • x) v₂) ∈ (p + q) • s
[PROOFSTEP]
exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : OrdConnected s
h : IsChain (fun x x_1 => x ≤ x_1) s
⊢ Convex 𝕜 s
[PROOFSTEP]
refine' convex_iff_segment_subset.mpr fun x hx y hy => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : OrdConnected s
h : IsChain (fun x x_1 => x ≤ x_1) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
⊢ [x-[𝕜]y] ⊆ s
[PROOFSTEP]
obtain hxy | hyx := h.total hx hy
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : OrdConnected s
h : IsChain (fun x x_1 => x ≤ x_1) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x-[𝕜]y] ⊆ s
[PROOFSTEP]
exact (segment_subset_Icc hxy).trans (hs.out hx hy)
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : OrdConnected s
h : IsChain (fun x x_1 => x ≤ x_1) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [x-[𝕜]y] ⊆ s
[PROOFSTEP]
rw [segment_symm]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝³ : OrderedSemiring 𝕜
inst✝² : OrderedAddCommMonoid E
inst✝¹ : Module 𝕜 E
inst✝ : OrderedSMul 𝕜 E
s : Set E
hs : OrdConnected s
h : IsChain (fun x x_1 => x ≤ x_1) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y-[𝕜]x] ⊆ s
[PROOFSTEP]
exact (segment_subset_Icc hyx).trans (hs.out hy hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
⊢ Convex 𝕜 s ↔ OrdConnected s
[PROOFSTEP]
simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
⊢ Convex 𝕜 ↑K
[PROOFSTEP]
repeat' intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
⊢ Convex 𝕜 ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
⊢ x✝ ∈ ↑K → StarConvex 𝕜 x✝ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝ : x✝ ∈ ↑K
⊢ StarConvex 𝕜 x✝ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝ : x✝ ∈ ↑K
y✝ : E
⊢ y✝ ∈ ↑K → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x✝ + b • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝¹ : x✝ ∈ ↑K
y✝ : E
a✝ : y✝ ∈ ↑K
⊢ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x✝ + b • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝² : x✝ ∈ ↑K
y✝ : E
a✝¹ : y✝ ∈ ↑K
a✝ : 𝕜
⊢ ∀ ⦃b : 𝕜⦄, 0 ≤ a✝ → 0 ≤ b → a✝ + b = 1 → a✝ • x✝ + b • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝² : x✝ ∈ ↑K
y✝ : E
a✝¹ : y✝ ∈ ↑K
a✝ b✝ : 𝕜
⊢ 0 ≤ a✝ → 0 ≤ b✝ → a✝ + b✝ = 1 → a✝ • x✝ + b✝ • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝³ : x✝ ∈ ↑K
y✝ : E
a✝² : y✝ ∈ ↑K
a✝¹ b✝ : 𝕜
a✝ : 0 ≤ a✝¹
⊢ 0 ≤ b✝ → a✝¹ + b✝ = 1 → a✝¹ • x✝ + b✝ • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁴ : x✝ ∈ ↑K
y✝ : E
a✝³ : y✝ ∈ ↑K
a✝² b✝ : 𝕜
a✝¹ : 0 ≤ a✝²
a✝ : 0 ≤ b✝
⊢ a✝² + b✝ = 1 → a✝² • x✝ + b✝ • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K
[PROOFSTEP]
intro
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • x✝ + b✝ • y✝ ∈ ↑K
[PROOFSTEP]
refine' add_mem (smul_mem _ _ _) (smul_mem _ _ _)
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ x✝ ∈ K
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
K : Submodule 𝕜 E
x✝ : E
a✝⁵ : x✝ ∈ ↑K
y✝ : E
a✝⁴ : y✝ ∈ ↑K
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ y✝ ∈ K
[PROOFSTEP]
assumption
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ stdSimplex 𝕜 ι = (⋂ (x : ι), {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
[PROOFSTEP]
ext f
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
⊢ f ∈ stdSimplex 𝕜 ι ↔ f ∈ (⋂ (x : ι), {f | 0 ≤ f x}) ∩ {f | ∑ x : ι, f x = 1}
[PROOFSTEP]
simp only [stdSimplex, Set.mem_inter_iff, Set.mem_iInter, Set.mem_setOf_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)
[PROOFSTEP]
refine' fun f hf g hg a b ha hb hab => ⟨fun x => _, _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x
[PROOFSTEP]
apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f + b • g) x = 1
[PROOFSTEP]
erw [Finset.sum_add_distrib]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f) x + ∑ x : ι, (b • g) x = 1
[PROOFSTEP]
simp only [Pi.smul_apply]
  -- Porting note: `erw` failed to rewrite with `← Finset.smul_sum`
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, a • f x + ∑ x : ι, b • g x = 1
[PROOFSTEP]
rw [← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul, smul_eq_mul, mul_one, mul_one]
[GOAL]
case refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b = 1
[PROOFSTEP]
exact hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
⊢ 0 ≤ (fun j => if i = j then 1 else 0) j
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
⊢ 0 ≤ if i = j then 1 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
h✝ : i = j
⊢ 0 ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i j : ι
h✝ : ¬i = j
⊢ 0 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
β : Type u_4
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
i : ι
⊢ ∑ x : ι, (fun j => if i = j then 1 else 0) x = 1
[PROOFSTEP]
rw [Finset.sum_ite_eq, if_pos (Finset.mem_univ _)]
