internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨x, hx⟩ := hsnonempty.combiInterior (K₁.indep hs)
Proof state after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hx.1⟩
Proof state after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : x ∈ K₁.space
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : x ∈ K₁.space
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
rw [hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
Proof state after:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain ⟨t, ht, hxt⟩ := hxspace
Proof state after:
case mpr.intro.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.intro.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
use t, ht
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull (K₁.indep hs)]
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Tactic:
refine' closure_minimal (fun x' hx' => _) (isClosed_convexHull _)
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
⊢ x' ∈ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hx'.1⟩
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : x' ∈ K₁.space
⊢ x' ∈ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : x' ∈ K₁.space
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
rw [hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
Proof state after:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x' ∈ combiInterior ℝ i
⊢ x' ∈ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₂), x' ∈ combiInterior ℝ i
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
obtain ⟨t', ht', hxt'⟩ := hxspace
Proof state after:
case right.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ x' ∈ (convexHull ℝ) ↑t
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case right.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ x' ∈ (convexHull ℝ) ↑t
Tactic:
convert hxt'.1
Proof state after:
case h.e'_5.h.e'_6.h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ t = t'
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case h.e'_5.h.e'_6.h.e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
⊢ t = t'
Tactic:
obtain ⟨F, hF, hinterior⟩ := hpartition _ ht
Proof state after:
case h.e'_5.h.e'_6.h.e'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ t = t'
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case h.e'_5.h.e'_6.h.e'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ t = t'
Tactic:
obtain ⟨F', hF', hinterior'⟩ := hpartition _ ht'
Proof state after:
case h.e'_5.h.e'_6.h.e'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ t = t'
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case h.e'_5.h.e'_6.h.e'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ t = t'
Tactic:
apply disjoint_interiors ht ht' (_ : x ∈ _) _
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t

𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t✝ : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace✝ : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
hxt' : x' ∈ combiInterior ℝ t'
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
⊢ x ∈ combiInterior ℝ t'
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ K₁.space = K₂.space
Tactic:
refine' hspace.antisymm fun x hx => _
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : x ∈ K₂.space
⊢ x ∈ K₁.space
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : x ∈ K₂.space
⊢ x ∈ K₁.space
Tactic:
rw [← combiInteriors_cover, mem_iUnion₂] at hx ⊢
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
hx : ∃ i, ∃ (_ : i ∈ K₂), x ∈ combiInterior ℝ i
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨s, hs, hxs⟩ := hx
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
Tactic:
obtain ⟨F, hF, hsint⟩ := hpartition _ hs
Proof state after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s✝ t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i