internlm/Lean-Github huggingface dataset:
Theorem: Sublattice.le_pi
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i
Tactic:
aesop
Proof state after:
no goals
Theorem: Sublattice.pi_univ_eq_bot
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ pi univ L = ⊥ ↔ ∃ i, L i = ⊥
Tactic:
simp_rw [← coe_inj]
Proof state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥
Theorem: Sublattice.pi_univ_eq_bot
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
⊢ ↑(pi univ L) = ↑⊥ ↔ ∃ i, ↑(L i) = ↑⊥
Tactic:
simp
Proof state after:
no goals
Theorem: mem_combiFrontier_iff
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ x ∈ combiFrontier 𝕜 s ↔ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
simp [combiFrontier]
Proof state after:
no goals
Theorem: combiFrontier_empty
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ = ∅
Tactic:
apply Set.eq_empty_of_subset_empty
Proof state after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ ⊆ ∅
Theorem: combiFrontier_empty
Proof state before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ ⊆ ∅
Tactic:
convert combiFrontier_subset_convexHull
Proof state after:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅
Theorem: combiFrontier_empty
Proof state before:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅
Tactic:
rw [Finset.coe_empty, convexHull_empty]
Proof state after:
no goals
Theorem: combiInterior_empty
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 ∅ = ∅
Tactic:
apply Set.eq_empty_of_subset_empty
Proof state after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 ∅ ⊆ ∅
Theorem: combiInterior_empty
Proof state before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 ∅ ⊆ ∅
Tactic:
convert combiInterior_subset_convexHull
Proof state after:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅
Theorem: combiInterior_empty
Proof state before:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅
Tactic:
rw [Finset.coe_empty, convexHull_empty]
Proof state after:
no goals
Theorem: combiFrontier_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 {x} = ∅
Tactic:
refine eq_empty_of_subset_empty fun y hy ↦ ?_
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : y ∈ combiFrontier 𝕜 {x}
⊢ y ∈ ∅
Theorem: combiFrontier_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : y ∈ combiFrontier 𝕜 {x}
⊢ y ∈ ∅
Tactic:
rw [mem_combiFrontier_iff] at hy
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : ∃ t ⊂ {x}, y ∈ (convexHull 𝕜) ↑t
⊢ y ∈ ∅
Theorem: combiFrontier_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : ∃ t ⊂ {x}, y ∈ (convexHull 𝕜) ↑t
⊢ y ∈ ∅
Tactic:
obtain ⟨s, hs, hys⟩ := hy
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑s
⊢ y ∈ ∅
Theorem: combiFrontier_singleton
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑s
⊢ y ∈ ∅
Tactic:
rw [Finset.eq_empty_of_ssubset_singleton hs] at hys
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑∅
⊢ y ∈ ∅
Theorem: combiFrontier_singleton
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑∅
⊢ y ∈ ∅
Tactic:
simp at hys
Proof state after:
no goals
Theorem: combiInterior_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiInterior 𝕜 {x} = {x}
Tactic:
unfold combiInterior
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑{x} \ combiFrontier 𝕜 {x} = {x}
Theorem: combiInterior_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑{x} \ combiFrontier 𝕜 {x} = {x}
Tactic:
rw [combiFrontier_singleton]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑{x} \ ∅ = {x}
Theorem: combiInterior_singleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑{x} \ ∅ = {x}
Tactic:
simp
Proof state after:
no goals
Theorem: simplex_combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s = ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
apply Subset.antisymm _ _
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ (convexHull 𝕜) ↑s
Theorem: simplex_combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
refine s.strongInductionOn ?_
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∀ (s : Finset E),
    (∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1) →
      (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∀ (s : Finset E),
    (∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1) →
      (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
rintro s ih x hx
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
by_cases h : x ∈ combiFrontier 𝕜 s
Proof state after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∈ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∉ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∈ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
rw [mem_combiFrontier_iff] at h
Proof state after:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
obtain ⟨t, st, ht⟩ := h
Proof state after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
specialize ih _ st ht
Proof state after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : x ∈ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : x ∈ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
simp only [exists_prop, Set.mem_iUnion] at ih ⊢
Proof state after:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : ∃ i ⊆ t, x ∈ combiInterior 𝕜 i
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
ih : ∃ i ⊆ t, x ∈ combiInterior 𝕜 i
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Tactic:
obtain ⟨Z, Zt, hZ⟩ := ih
Proof state after:
case pos.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
Z : Finset E
Zt : Z ⊆ t
hZ : x ∈ combiInterior 𝕜 Z
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Theorem: simplex_combiInteriors_cover
Proof state before:
case pos.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ : Finset E
x✝ : E
s : Finset E
x : E
hx : x ∈ (convexHull 𝕜) ↑s
t : Finset E
st : t ⊂ s
ht : x ∈ (convexHull 𝕜) ↑t
Z : Finset E
Zt : Z ⊆ t
hZ : x ∈ combiInterior 𝕜 Z
⊢ ∃ i ⊆ s, x ∈ combiInterior 𝕜 i
Tactic:
exact ⟨_, Zt.trans st.1, hZ⟩
Proof state after:
no goals
Theorem: simplex_combiInteriors_cover
Proof state before:
case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x✝ : E
s : Finset E
ih : ∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1
x : E
hx : x ∈ (convexHull 𝕜) ↑s
h : x ∉ combiFrontier 𝕜 s
⊢ x ∈ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
Tactic:
exact subset_iUnion₂ s Subset.rfl ⟨hx, h⟩
Proof state after:
no goals
Theorem: simplex_combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ (convexHull 𝕜) ↑s
Tactic:
exact iUnion₂_subset fun t ht ↦ diff_subset.trans $ convexHull_mono ht
Proof state after:
no goals
Theorem: combiFrontier_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
⊢ combiFrontier 𝕜 s =
    {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Tactic:
ext x
Proof state after:
case h
𝕜 : 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 ∈ combiFrontier 𝕜 s ↔
    x ∈ {x | ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x}
Theorem: combiFrontier_eq
Proof state before:
case h
𝕜 : 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 ∈ combiFrontier 𝕜 s ↔
    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_rw [combiFrontier, Set.mem_iUnion, Set.mem_setOf_eq]
Proof state after:
case h
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) ↔
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) ↔
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x
Tactic:
constructor
Proof state after:
case h.mp
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) →
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x

case h.mpr
𝕜 : 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, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x) →
    ∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i
Theorem: combiFrontier_eq
Proof state before:
case h.mp
𝕜 : 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
⊢ (∃ i, ∃ (_ : i ⊂ s), x ∈ (convexHull 𝕜) ↑i) →
    ∃ w, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x
Tactic:
simp only [and_imp, exists_prop, exists_imp]
Proof state after:
case h.mp
𝕜 : 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 ⊂ s,
    x ∈ (convexHull 𝕜) ↑x_1 → ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp
𝕜 : 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 ⊂ s,
    x ∈ (convexHull 𝕜) ↑x_1 → ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
intro t ts hx
Proof state after:
case h.mp
𝕜 : 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
t : Finset E
ts : t ⊂ s
hx : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp
𝕜 : 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
t : Finset E
ts : t ⊂ s
hx : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rw [Finset.convexHull_eq, Set.mem_setOf_eq] at hx
Proof state after:
case h.mp
𝕜 : 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
t : Finset E
ts : t ⊂ s
hx : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp
𝕜 : 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
t : Finset E
ts : t ⊂ s
hx : ∃ w, (∀ y ∈ t, 0 ≤ w y) ∧ ∑ y ∈ t, w y = 1 ∧ t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rcases hx with ⟨w, hw₀, hw₁, hx⟩
Proof state after:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
rcases Finset.exists_of_ssubset ts with ⟨y, hys, hyt⟩
Proof state after:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
let w' z := if z ∈ t then w z else 0
Proof state after:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Theorem: combiFrontier_eq
Proof state before:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x
Tactic:
have hw'₁ : s.sum w' = 1 := by
  rwa [← Finset.sum_subset ts.1, Finset.sum_extend_by_zero]
  simp only [ite_eq_right_iff]
  tauto
Proof state after:
case h.mp.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✝ x : E
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y : E
hys : y ∈ s
hyt : y ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
⊢ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ (∃ y ∈ s, w y = 0) ∧ s.centerMass w id = x