internlm/Lean-Github huggingface dataset:
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
Tactic:
rwa [Finset.centerMass_subset _ (s.erase_subset _)]
Proof state after:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∀ i ∈ s, i ∉ s.erase y → w i = 0
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∀ i ∈ s, i ∉ s.erase y → w i = 0
Tactic:
intro i hi₁ hi₂
Proof state after:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
i : E
hi₁ : i ∈ s
hi₂ : i ∉ s.erase y
⊢ w i = 0
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
i : E
hi₁ : i ∈ s
hi₂ : i ∉ s.erase y
⊢ w i = 0
Tactic:
simp only [hi₁, and_true_iff, Classical.not_not, Finset.mem_erase] at hi₂
Proof state after:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
i : E
hi₁ : i ∈ s
hi₂ : i = y
⊢ w i = 0
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
i : E
hi₁ : i ∈ s
hi₂ : i = y
⊢ w i = 0
Tactic:
subst hi₂
Proof state after:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hy₃ : s.centerMass w id = x
i : E
hi₁ hy₁ : i ∈ s
hy₂ : w i = 0
⊢ w i = 0
Theorem: combiFrontier_eq
Proof state before:
case h.mpr.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hy₃ : s.centerMass w id = x
i : E
hi₁ hy₁ : i ∈ s
hy₂ : w i = 0
⊢ w i = 0
Tactic:
apply hy₂
Proof state after:
no goals
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 s ⊆ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rw [combiInterior, Finset.convexHull_eq, combiFrontier_eq]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
      {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} ⊆
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
      {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} ⊆
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rintro x
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} →
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x} →
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∀ (x_2 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_2 y) → ∑ y ∈ s, x_2 y = 1 → ∀ x_5 ∈ s, x_2 x_5 = 0 → ¬s.centerMass x_2 id = x) →
            ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∀ (x_2 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_2 y) → ∑ y ∈ s, x_2 y = 1 → ∀ x_5 ∈ s, x_2 x_5 = 0 → ¬s.centerMass x_2 id = x) →
            ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Tactic:
rintro w hw₁ hw₂ hw₃ q
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
⊢ ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
⊢ ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
Tactic:
refine' ⟨w, fun y hy => _, hw₂, hw₃⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
y : E
hy : y ∈ s
⊢ 0 < w y
Theorem: combiInterior_subset_positive_weighings
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
y : E
hy : y ∈ s
⊢ 0 < w y
Tactic:
exact lt_of_le_of_ne (hw₁ _ hy) (Ne.symm fun t => q w hw₁ hw₂ y hy t hw₃)
Proof state after:
no goals
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
⊢ combiInterior 𝕜 s = {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' combiInterior_subset_positive_weighings.antisymm fun x => _
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} → x ∈ combiInterior 𝕜 s
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} → x ∈ combiInterior 𝕜 s
Tactic:
rw [combiInterior, Finset.convexHull_eq, combiFrontier_eq]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
    x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
    x ∈
      {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x} \
        {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Tactic:
simp only [not_exists, and_imp, not_and, mem_setOf_eq, mem_diff, exists_imp]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 < x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
            ∀ (x_4 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_4 y) → ∑ y ∈ s, x_4 y = 1 → ∀ x_7 ∈ s, x_4 x_7 = 0 → ¬s.centerMass x_4 id = x
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 < x_1 y) →
      ∑ y ∈ s, x_1 y = 1 →
        s.centerMass x_1 id = x →
          (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
            ∀ (x_4 : E → 𝕜),
              (∀ y ∈ s, 0 ≤ x_4 y) → ∑ y ∈ s, x_4 y = 1 → ∀ x_7 ∈ s, x_4 x_7 = 0 → ¬s.centerMass x_4 id = x
Tactic:
intro w hw₀ hw₁ hw₂
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
    ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
⊢ (∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x) ∧
    ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
Tactic:
refine' ⟨⟨w, fun y hy => (hw₀ y hy).le, hw₁, hw₂⟩, fun v hv₀ hv₁ y hy hvy hv₂ => (hw₀ y hy).ne' _⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
hw₂ : s.centerMass w id = x
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [← hv₂] at hw₂
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : s.centerMass w id = s.centerMass v id
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : s.centerMass w id = s.centerMass v id
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [Finset.centerMass_eq_of_sum_1 _ _ hv₁, Finset.centerMass_eq_of_sum_1 _ _ hw₁] at hw₂
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
Tactic:
rw [← hvy]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = v y
Theorem: combiInterior_eq
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = v y
Tactic:
exact hs.eq_of_sum_eq_sum_subtype (hw₁.trans hv₁.symm) hw₂ _ hy
Proof state after:
no goals
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ Finset.centroid 𝕜 s id ∈ combiInterior 𝕜 s
Tactic:
rw [Finset.centroid_def]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Tactic:
have hsweights := s.sum_centroidWeights_eq_one_of_nonempty 𝕜 hs'
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ (Finset.affineCombination 𝕜 s id) (Finset.centroidWeights 𝕜 s) ∈ combiInterior 𝕜 s
Tactic:
rw [affineCombination_eq_centerMass hsweights]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈ combiInterior 𝕜 s
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈ combiInterior 𝕜 s
Tactic:
rw [combiInterior_eq hs]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
⊢ s.centerMass (fun i => Finset.centroidWeights 𝕜 s i) id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
refine' ⟨_, fun y _ => _, hsweights, rfl⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
y : E
x✝ : y ∈ s
⊢ 0 < Finset.centroidWeights 𝕜 s y
Theorem: centroid_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
hs' : s.Nonempty
hsweights : ∑ i ∈ s, Finset.centroidWeights 𝕜 s i = 1
y : E
x✝ : y ∈ s
⊢ 0 < Finset.centroidWeights 𝕜 s y
Tactic:
simpa using hs'.card_pos
Proof state after:
no goals
Theorem: convex_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
⊢ Convex 𝕜 (combiInterior 𝕜 s)
Tactic:
simp_rw [convex_iff_forall_pos, combiInterior_eq hs]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
⊢ ∀ ⦃x : E⦄,
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
      ∀ ⦃y : E⦄,
        y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
          ∀ ⦃a b : 𝕜⦄,
            0 < a →
              0 < b →
                a + b = 1 →
                  a • x + b • y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Theorem: convex_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
⊢ ∀ ⦃x : E⦄,
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
      ∀ ⦃y : E⦄,
        y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x} →
          ∀ ⦃a b : 𝕜⦄,
            0 < a →
              0 < b →
                a + b = 1 →
                  a • x + b • y ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}
Tactic:
rintro x ⟨v, hv₀, hv₁, rfl⟩ y ⟨w, hw₀, hw₁, rfl⟩ a b ha hb h
Proof state after:
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
hs : AffineIndependent 𝕜 Subtype.val
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ a • s.centerMass v id + b • s.centerMass w id ∈
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x}