internlm/Lean-Github huggingface dataset:
Theorem: Finset.mem_posSub
Proof state before:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s -₊ t ↔ ∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = a
Tactic:
simp_rw [posSub, mem_image, mem_filter, mem_product, Prod.exists, and_assoc, exists_and_left]
Proof state after:
no goals
Theorem: Finset.posSub_subset_sub
Proof state before:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ x ∈ s -₊ t → x ∈ s - t
Tactic:
rw [mem_posSub, mem_sub]
Proof state after:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = x) → ∃ b ∈ s, ∃ c ∈ t, b - c = x
Theorem: Finset.posSub_subset_sub
Proof state before:
α : Type u_1
inst✝³ : Sub α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : DecidableEq α
s t : Finset α
a x : α
⊢ (∃ b ∈ s, ∃ c ∈ t, c ≤ b ∧ b - c = x) → ∃ b ∈ s, ∃ c ∈ t, b - c = x
Tactic:
exact fun ⟨b, hb, c, hc, _, h⟩ ↦ ⟨b, hb, c, hc, h⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
⊢ s = t
Tactic:
classical
by_contra h
have hst : s ∩ t ⊂ s := by
  use inter_subset_left
  intro H
  exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
    fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
refine' hxs.2 (Set.mem_biUnion hst _)
push_cast
exact K.inter_subset_convexHull hs ht ⟨hxs.1, hxt.1⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
⊢ s = t
Tactic:
by_contra h
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ False
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ False
Tactic:
have hst : s ∩ t ⊂ s := by
  use inter_subset_left
  intro H
  exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
    fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ False
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ False
Tactic:
refine' hxs.2 (Set.mem_biUnion hst _)
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) ↑(s ∩ t)
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) ↑(s ∩ t)
Tactic:
push_cast
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) (↑s ∩ ↑t)
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
hst : s ∩ t ⊂ s
⊢ x ∈ (convexHull 𝕜) (↑s ∩ ↑t)
Tactic:
exact K.inter_subset_convexHull hs ht ⟨hxs.1, hxt.1⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ s ∩ t ⊂ s
Tactic:
use inter_subset_left
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ ¬s ⊆ s ∩ t
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
⊢ ¬s ⊆ s ∩ t
Tactic:
intro H
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
H : s ⊆ s ∩ t
⊢ False
Theorem: Geometry.SimplicialComplex.disjoint_interiors
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ combiInterior 𝕜 t
h : ¬s = t
H : s ⊆ s ∩ t
⊢ False
Tactic:
exact hxt.2 $ Set.mem_biUnion ⟨H.trans inter_subset_right,
  fun H2 => h $ (H.trans inter_subset_right).antisymm H2⟩ hxs.1
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.eq_singleton_of_singleton_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ s = {x}
Tactic:
apply disjoint_interiors hs hx hxs
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ combiInterior 𝕜 {x}
Theorem: Geometry.SimplicialComplex.eq_singleton_of_singleton_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ combiInterior 𝕜 {x}
Tactic:
rw [combiInterior_singleton]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ {x}
Theorem: Geometry.SimplicialComplex.eq_singleton_of_singleton_mem_combiInterior
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : {x} ∈ K
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ x ∈ {x}
Tactic:
exact Set.mem_singleton x
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = K.space
Tactic:
unfold space
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ ⋃ s ∈ K, combiInterior 𝕜 s = ⋃ s ∈ K.faces, (convexHull 𝕜) ↑s
Tactic:
refine' (Set.iUnion₂_mono fun _ _ => _).antisymm (Set.iUnion₂_subset fun s hs => _)
Proof state after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
x✝¹ : Finset E
x✝ : x✝¹ ∈ K
⊢ combiInterior 𝕜 x✝¹ ⊆ (convexHull 𝕜) ↑x✝¹

case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Tactic:
rw [simplex_combiInteriors_cover]
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
⊢ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t ⊆ ⋃ i ∈ K, combiInterior 𝕜 i
Tactic:
refine' Set.iUnion₂_mono' fun t hts => _
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
Proof state after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 i'

case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
ht : t.Nonempty
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
x✝¹ : Finset E
x✝ : x✝¹ ∈ K
⊢ combiInterior 𝕜 x✝¹ ⊆ (convexHull 𝕜) ↑x✝¹
Tactic:
exact combiInterior_subset_convexHull
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 i'
Tactic:
refine' ⟨s, hs, _⟩
Proof state after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 s
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ combiInterior 𝕜 ∅ ⊆ combiInterior 𝕜 s
Tactic:
rw [combiInterior_empty]
Proof state after:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∅ ⊆ combiInterior 𝕜 s
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
hts : ∅ ⊆ s
⊢ ∅ ⊆ combiInterior 𝕜 s
Tactic:
exact Set.empty_subset _
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.combiInteriors_cover
Proof state before:
case refine'_2.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
s : Finset E
hs : s ∈ K
t : Finset E
hts : t ⊆ s
ht : t.Nonempty
⊢ ∃ i', ∃ (_ : i' ∈ K), combiInterior 𝕜 t ⊆ combiInterior 𝕜 i'
Tactic:
exact ⟨t, K.down_closed' hs hts ht, Set.Subset.rfl⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.combiInteriors_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ K.space
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
rw [← combiInteriors_cover] at hx
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Theorem: Geometry.SimplicialComplex.combiInteriors_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
obtain ⟨s, hs, hxs⟩ := Set.mem_iUnion₂.1 hx
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
s : Finset E
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Theorem: Geometry.SimplicialComplex.combiInteriors_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
hx : x ∈ ⋃ s ∈ K, combiInterior 𝕜 s
s : Finset E
hs : s ∈ K
hxs : x ∈ combiInterior 𝕜 s
⊢ ∃! s, s ∈ K ∧ x ∈ combiInterior 𝕜 s
Tactic:
exact ⟨s, ⟨⟨hs, hxs⟩, fun t ⟨ht, hxt⟩ => disjoint_interiors ht hs hxt hxs⟩⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_convexHull_iff
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ x ∈ (convexHull 𝕜) ↑s ↔ ∃ t ⊆ s, x ∈ combiInterior 𝕜 t
Tactic:
simp [simplex_combiInteriors_cover]
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ x ∈ combiFrontier 𝕜 s ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
rw [mem_combiFrontier_iff]
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) ↔ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
constructor
Proof state after:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) → ∃ t ⊂ s, x ∈ combiInterior 𝕜 t

case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ combiInterior 𝕜 t) → ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
case mp
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t) → ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
rintro ⟨t, hts, hxt⟩
Proof state after:
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ ∃ t ⊂ s, x ∈ combiInterior 𝕜 t
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
case mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
⊢ (∃ t ⊂ s, x ∈ combiInterior 𝕜 t) → ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
rintro ⟨t, hts, hxt⟩
Proof state after:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ combiInterior 𝕜 t
⊢ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Theorem: Geometry.SimplicialComplex.mem_combiFrontier_iff'
Proof state before:
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t✝ : Finset E
A : Set (Finset E)
m n : ℕ
t : Finset E
hts : t ⊂ s
hxt : x ∈ combiInterior 𝕜 t
⊢ ∃ t ⊂ s, x ∈ (convexHull 𝕜) ↑t
Tactic:
exact ⟨t, hts, hxt.1⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subset_of_combiInterior_inter_convexHull_nonempty
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hst : (combiInterior 𝕜 s ∩ (convexHull 𝕜) ↑t).Nonempty
⊢ s ⊆ t
Tactic:
obtain ⟨x, hxs, hxt⟩ := hst
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ s ⊆ t
Theorem: Geometry.SimplicialComplex.subset_of_combiInterior_inter_convexHull_nonempty
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ s ⊆ t
Tactic:
obtain ⟨u, hut, hxu⟩ := mem_convexHull_iff.1 hxt
Proof state after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ s ⊆ t