internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.subset_of_combiInterior_inter_convexHull_nonempty
Proof state before:
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
Tactic:
rw [disjoint_interiors hs (K.down_closed' ht hut <| nonempty_of_ne_empty _) hxs hxu]
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
⊢ u ⊆ t

𝕜 : 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
⊢ u ≠ ∅
Theorem: Geometry.SimplicialComplex.subset_of_combiInterior_inter_convexHull_nonempty
Proof state before:
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
⊢ u ⊆ t

𝕜 : 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
⊢ u ≠ ∅
Tactic:
exact hut
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
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅
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
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅
Tactic:
rintro rfl
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
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
hut : ∅ ⊆ t
hxu : x ∈ combiInterior 𝕜 ∅
⊢ False
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
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
hut : ∅ ⊆ t
hxu : x ∈ combiInterior 𝕜 ∅
⊢ False
Tactic:
rwa [combiInterior_empty] at hxu
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ K.cells ⊆ K.facets
Tactic:
rintro s ⟨hs, hscard⟩
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
⊢ s ∈ K.facets
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
⊢ s ∈ K.facets
Tactic:
by_contra h
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
⊢ False
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
⊢ False
Tactic:
obtain ⟨t, ht, hst⟩ := (not_facet_iff_subface hs).mp h
Proof state after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
⊢ False
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
⊢ False
Tactic:
have := card_lt_card hst
Proof state after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this : s.card < t.card
⊢ False
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this : s.card < t.card
⊢ False
Tactic:
have := face_dimension_le_space_dimension ht
Proof state after:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this✝ : s.card < t.card
this : t.card ≤ FiniteDimensional.finrank 𝕜 E + 1
⊢ False
Theorem: Geometry.SimplicialComplex.cells_subset_facets
Proof state before:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
s : Finset E
hs : s ∈ K
hscard : s.card = FiniteDimensional.finrank 𝕜 E + 1
h : s ∉ K.facets
t : Finset E
ht : t ∈ K.faces
hst : s ⊂ t
this✝ : s.card < t.card
this : t.card ≤ FiniteDimensional.finrank 𝕜 E + 1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
classical
let K := SimplicialComplex.ofSimplex ht
let F := t.powerset.filter fun v : Finset E => (s : Set E) ⊆ convexHull 𝕜 ↑v
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
let K := SimplicialComplex.ofSimplex ht
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
let F := t.powerset.filter fun v : Finset E => (s : Set E) ⊆ convexHull 𝕜 ↑v
Proof state after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
F : Finset (Finset E) := filter (fun v => ↑s ⊆ (convexHull 𝕜) ↑v) t.powerset
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K✝ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
K : SimplicialComplex 𝕜 E := ofSimplex ht
F : Finset (Finset E) := filter (fun v => ↑s ⊆ (convexHull 𝕜) ↑v) t.powerset
⊢ ∃ u ⊆ t, combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.simplex_combiInteriors_split_interiors_nonempty
Proof state before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s.Nonempty
ht : AffineIndependent 𝕜 Subtype.val
hst : (convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t
⊢ ∃ u ⊆ t, u.Nonempty ∧ combiInterior 𝕜 s ⊆ combiInterior 𝕜 u
Tactic:
sorry
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
⊢ (K.skeleton k).faces.Nonempty ↔ K.faces.Nonempty
Tactic:
refine' ⟨Set.Nonempty.mono skeleton_le, _⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
⊢ K.faces.Nonempty → (K.skeleton k).faces.Nonempty
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
⊢ K.faces.Nonempty → (K.skeleton k).faces.Nonempty
Tactic:
rintro ⟨s, hs⟩
Proof state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
⊢ (K.skeleton k).faces.Nonempty
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
⊢ (K.skeleton k).faces.Nonempty
Tactic:
obtain ⟨x, hx⟩ := K.nonempty hs
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ (K.skeleton k).faces.Nonempty
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ (K.skeleton k).faces.Nonempty
Tactic:
refine' ⟨{x}, K.down_closed' hs (singleton_subset_iff.2 hx) <| singleton_nonempty _, _⟩
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ {x}.card ≤ k + 1
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ {x}.card ≤ k + 1
Tactic:
rw [card_singleton]
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ 1 ≤ k + 1
Theorem: Geometry.SimplicialComplex.skeleton_nonempty_iff
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
s : Finset E
hs : s ∈ K.faces
x : E
hx : x ∈ s
⊢ 1 ≤ k + 1
Tactic:
exact le_add_self
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.skeleton_of_le
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ (K.skeleton k).Pure k
Tactic:
refine' ⟨fun s hs => hs.2, _⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ Set.Sized (k + 1) (K.skeleton k).facets
Theorem: Geometry.SimplicialComplex.Pure.skeleton_of_le
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ Set.Sized (k + 1) (K.skeleton k).facets
Tactic:
rintro s ⟨⟨hs, hscard⟩, hsmax⟩
Proof state after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
⊢ s.card = k + 1
Theorem: Geometry.SimplicialComplex.Pure.skeleton_of_le
Proof state before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
⊢ s.card = k + 1
Tactic:
obtain ⟨t, ht, hst, htcard⟩ := hK.exists_face_of_card_le (add_le_add_right h 1) hs hscard
Proof state after:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
t : Finset E
ht : t ∈ K
hst : s ⊆ t
htcard : t.card = k + 1
⊢ s.card = k + 1
Theorem: Geometry.SimplicialComplex.Pure.skeleton_of_le
Proof state before:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
s : Finset E
hsmax : ∀ ⦃t : Finset E⦄, t ∈ (K.skeleton k).faces → s ⊆ t → s = t
hs : s ∈ K
hscard : s.card ≤ k + 1
t : Finset E
ht : t ∈ K
hst : s ⊆ t
htcard : t.card = k + 1
⊢ s.card = k + 1
Tactic:
rwa [hsmax ⟨ht, htcard.le⟩ hst]
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
⊢ (K.skeleton k).Pure (min k n)
Tactic:
obtain hn | hn := le_total k n
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure (min k n)

case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure (min k n)
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure (min k n)
Tactic:
rw [min_eq_left hn]
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure k
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : k ≤ n
⊢ (K.skeleton k).Pure k
Tactic:
exact hK.skeleton_of_le hn
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure (min k n)
Tactic:
rw [min_eq_right hn]
Proof state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure n
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure n
Tactic:
refine' ⟨fun s hs => hK.1 <| skeleton_le hs, fun s hs => _⟩
Proof state after:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
⊢ s.card = n + 1
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
⊢ s.card = n + 1
Tactic:
obtain ⟨t, ht, hst⟩ := subfacet (skeleton_le hs.1)
Proof state after:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ s.card = n + 1
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ s.card = n + 1
Tactic:
rw [hs.2 ⟨facets_subset ht, (hK.2 ht).le.trans (add_le_add_right hn _)⟩ hst]
Proof state after:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ t.card = n + 1
Theorem: Geometry.SimplicialComplex.Pure.skeleton
Proof state before:
case inr.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t✝ : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
t : Finset E
ht : t ∈ K.facets
hst : s ⊆ t
⊢ t.card = n + 1
Tactic:
exact hK.2 ht
Proof state after:
no goals
Theorem: List.getLast_filter
Proof state before:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p ([a].getLast ⋯) = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯
Tactic:
rw [List.getLast_singleton'] at h'
Proof state after:
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a : α
h : filter p [a] ≠ []
h' : p a = true
⊢ (filter p [a]).getLast h = [a].getLast ⋯