internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
⊢ K₁.faces.Nonempty → K₂.faces.Nonempty
Tactic:
rintro ⟨s₁, hs₁⟩
Proof state after:
case mp.intro.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
⊢ K₂.faces.Nonempty
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
⊢ K₂.faces.Nonempty
Tactic:
obtain ⟨s₂, hs₂, -⟩ := hsubdiv hs₁
Proof state after:
case mp.intro.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
s₂ : Finset E
hs₂ : s₂ ∈ K₂
⊢ K₂.faces.Nonempty
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
s₂ : Finset E
hs₂ : s₂ ∈ K₂
⊢ K₂.faces.Nonempty
Tactic:
exact ⟨s₂, hs₂⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
have hxspace := mem_space_iff.2 ⟨s, hs, hxs.1⟩
Proof state after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : x ∈ K₂.space
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : x ∈ K₂.space
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
rw [← hspace, ← combiInteriors_cover, mem_iUnion₂] at hxspace
Proof state after:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1
𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
hxspace : ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
obtain ⟨t, ht, hxt⟩ := hxspace
Proof state after:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁
Tactic:
refine' mem_iUnion₂_of_mem ⟨ht, fun y hyt => _⟩ hxt
Proof state after:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
⊢ y ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
⊢ y ∈ combiInterior ℝ s
Tactic:
obtain ⟨u, hu, htu⟩ := hsubdiv ht
Proof state after:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
⊢ y ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
⊢ y ∈ combiInterior ℝ s
Tactic:
obtain ⟨W, hWu, htW⟩ := simplex_combiInteriors_split_interiors (K₂.indep hu) htu
Proof state after:
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ s
Tactic:
rw [disjoint_interiors hs (K₂.down_closed hu hWu _) hxs (htW hxt)]
Proof state after:
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ W

𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ W

𝕜 : 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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
Tactic:
exact htW hyt
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅
Tactic:
rintro rfl
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
⊢ False
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
⊢ False
Tactic:
have := htW hxt
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
this : x ∈ combiInterior ℝ ∅
⊢ False
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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
hWu : ∅ ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ ∅
this : x ∈ combiInterior ℝ ∅
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁ → x ∈ combiInterior ℝ s
Tactic:
rw [mem_iUnion₂]
Proof state after:
case mp.intro.refine'_2.h.refine'_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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ (∃ i, ∃ (_ : i ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}), x ∈ combiInterior ℝ i) → x ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
⊢ (∃ i, ∃ (_ : i ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}), x ∈ combiInterior ℝ i) → x ∈ combiInterior ℝ s
Tactic:
rintro ⟨t, ⟨-, hts⟩, hxt⟩
Proof state after:
case mp.intro.refine'_2.h.refine'_2.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
t : Finset E
hxt : x ∈ combiInterior ℝ t
hts : combiInterior ℝ t ⊆ combiInterior ℝ s
⊢ x ∈ combiInterior ℝ s
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mp.intro.refine'_2.h.refine'_2.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s : Finset E
hs : s ∈ K₂
x : E
t : Finset E
hxt : x ∈ combiInterior ℝ t
hts : combiInterior ℝ t ⊆ combiInterior ℝ s
⊢ x ∈ combiInterior ℝ s
Tactic:
exact hts hxt
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr
𝕜 : 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
⊢ ((K₁.faces.Nonempty → K₂.faces.Nonempty) ∧
      K₁.space ⊆ K₂.space ∧ ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁) →
    K₁.Subdivides K₂
Tactic:
rintro ⟨hempty, hspace, hpartition⟩
Proof state after:
case mpr.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₁
⊢ K₁.Subdivides K₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.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₁
⊢ K₁.Subdivides K₂
Tactic:
have hspace : K₁.space = K₂.space := by
  refine' hspace.antisymm fun x hx => _
  rw [← combiInteriors_cover, mem_iUnion₂] at hx ⊢
  obtain ⟨s, hs, hxs⟩ := hx
  obtain ⟨F, hF, hsint⟩ := hpartition _ hs
  rw [hsint, mem_iUnion₂] at hxs
  obtain ⟨t, ht, hxt⟩ := hxs
  exact ⟨t, hF ht, hxt⟩
Proof state after:
case mpr.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
⊢ K₁.Subdivides K₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.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
⊢ K₁.Subdivides K₂
Tactic:
refine' ⟨hspace, fun s hs => _⟩
Proof state after:
case mpr.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₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Theorem: Geometry.SimplicialComplex.subdivides_iff_partition
Proof state before:
case mpr.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₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑s₂
Tactic:
obtain rfl | hsnonempty := s.eq_empty_or_nonempty
Proof state after:
case mpr.intro.intro.inl
𝕜 : 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
hs : ∅ ∈ K₁
⊢ ∃ s₂ ∈ K₂, (convexHull ℝ) ↑∅ ⊆ (convexHull ℝ) ↑s₂

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₂