internlm/Lean-Github huggingface dataset:
Theorem: Geometry.SimplicialComplex.not_mem_bot
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 ∉ ⊥
Tactic:
simp [← mem_faces_iff]
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.eq_bot_of_forall_not_mem
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 : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
⊢ K = ⊥
Tactic:
ext s
Proof state after:
case faces.h
𝕜 : 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 : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Theorem: Geometry.SimplicialComplex.eq_bot_of_forall_not_mem
Proof state before:
case faces.h
𝕜 : 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 : ℕ
K : SimplicialComplex 𝕜 E
h : ∀ (s : Finset E), s ∉ K
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Tactic:
exact iff_of_false (h s) id
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.space_eq_empty
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 : ℕ
⊢ K.space = ∅ ↔ K = ⊥
Tactic:
simp only [Set.eq_empty_iff_forall_not_mem, mem_space_iff, SimplicialComplex.ext_iff,
  @forall_swap E, mem_faces_iff, exists_prop, not_exists, not_and, faces_bot]
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 : ℕ
⊢ (∀ y ∈ K, ∀ (x : E), x ∉ (convexHull 𝕜) ↑y) ↔ ∀ (x : Finset E), x ∉ K
Theorem: Geometry.SimplicialComplex.space_eq_empty
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 : ℕ
⊢ (∀ y ∈ K, ∀ (x : E), x ∉ (convexHull 𝕜) ↑y) ↔ ∀ (x : Finset E), x ∉ K
Tactic:
simp only [← Set.eq_empty_iff_forall_not_mem, convexHull_empty_iff, coe_eq_empty]
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 : ℕ
⊢ (∀ y ∈ K, y = ∅) ↔ ∀ (x : Finset E), x ∉ K
Theorem: Geometry.SimplicialComplex.space_eq_empty
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 : ℕ
⊢ (∀ y ∈ K, y = ∅) ↔ ∀ (x : Finset E), x ∉ K
Tactic:
exact forall₂_congr fun s hs ↦ iff_false_intro (K.nonempty hs).ne_empty
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.coe_eq_empty
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 : ℕ
⊢ ↑K = ∅ ↔ K = ⊥
Tactic:
simp [Set.eq_empty_iff_forall_not_mem, SimplicialComplex.ext_iff]
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.facets_singleton
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 : ℕ
hK : K.faces = {s}
⊢ K.facets = {s}
Tactic:
rw [Set.eq_singleton_iff_unique_mem] at hK ⊢
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 : ℕ
hK : s ∈ K.faces ∧ ∀ x ∈ K.faces, x = s
⊢ s ∈ K.facets ∧ ∀ x ∈ K.facets, x = s
Theorem: Geometry.SimplicialComplex.facets_singleton
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 : ℕ
hK : s ∈ K.faces ∧ ∀ x ∈ K.faces, x = s
⊢ s ∈ K.facets ∧ ∀ x ∈ K.facets, x = s
Tactic:
exact ⟨⟨hK.1, fun t ht _ => (hK.2 _ ht).symm⟩, fun t ht => hK.2 _ ht.1⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_of_mem_convexHull
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.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s
Tactic:
have h := K.inter_subset_convexHull hx hs ⟨by simp, 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.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s
Theorem: Geometry.SimplicialComplex.mem_of_mem_convexHull
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.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s
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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
Theorem: Geometry.SimplicialComplex.mem_of_mem_convexHull
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.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
Tactic:
rwa [← coe_inter, inter_comm, disjoint_iff_inter_eq_empty.1 (disjoint_singleton_right.2 H),
  coe_empty, convexHull_empty] at h
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_of_mem_convexHull
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.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ (convexHull 𝕜) ↑{x}
Tactic:
simp
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.mem_ofSimplex
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 : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs ↔ t.Nonempty ∧ t ⊆ s
Tactic:
refine' ⟨_, fun h => ⟨h.1, s, rfl, h.2⟩⟩
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 : ℕ
hs : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs → t.Nonempty ∧ t ⊆ s
Theorem: Geometry.SimplicialComplex.mem_ofSimplex
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 : AffineIndependent 𝕜 Subtype.val
⊢ t ∈ ofSimplex hs → t.Nonempty ∧ t ⊆ s
Tactic:
rintro ⟨ht, u, rfl : u = s, hts⟩
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
t : Finset E
A : Set (Finset E)
m n : ℕ
ht : t.Nonempty
u : Finset E
hts : t ⊆ u
hs : AffineIndependent 𝕜 Subtype.val
⊢ t.Nonempty ∧ t ⊆ u
Theorem: Geometry.SimplicialComplex.mem_ofSimplex
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
t : Finset E
A : Set (Finset E)
m n : ℕ
ht : t.Nonempty
u : Finset E
hts : t ⊆ u
hs : AffineIndependent 𝕜 Subtype.val
⊢ t.Nonempty ∧ t ⊆ u
Tactic:
exact ⟨ht, hts⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.face_dimension_le_space_dimension
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
hs : s ∈ K
⊢ s.card ≤ FiniteDimensional.finrank 𝕜 E + 1
Tactic:
simpa using (K.indep hs).card_le_finrank_succ.trans (add_le_add_right (Submodule.finrank_le _) _)
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subfacet
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
hs : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
have := id hs
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 : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs this : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Theorem: Geometry.SimplicialComplex.subfacet
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
hs this : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
revert this
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 : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ s ∈ K → ∃ t ∈ K.facets, s ⊆ t
Theorem: Geometry.SimplicialComplex.subfacet
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
hs : s ∈ K
⊢ s ∈ K → ∃ t ∈ K.facets, s ⊆ t
Tactic:
refine strongDownwardInductionOn s ?_ (face_dimension_le_space_dimension hs)
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 : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
⊢ ∀ (t₁ : Finset E),
    (∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t) →
      t₁.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ∈ K → ∃ t ∈ K.facets, t₁ ⊆ t
Theorem: Geometry.SimplicialComplex.subfacet
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
hs : s ∈ K
⊢ ∀ (t₁ : Finset E),
    (∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t) →
      t₁.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t₁ ∈ K → ∃ t ∈ K.facets, t₁ ⊆ t
Tactic:
rintro t h - 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 : ℕ
inst✝ : FiniteDimensional 𝕜 E
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Theorem: Geometry.SimplicialComplex.subfacet
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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
by_cases htfacet : t ∈ K.facets
Proof state after:
case pos
𝕜 : 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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∈ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1

case neg
𝕜 : 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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Theorem: Geometry.SimplicialComplex.subfacet
Proof state before:
case neg
𝕜 : 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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
obtain ⟨u, hu, htu⟩ := (not_facet_iff_subface ht).mp htfacet
Proof state after:
case neg.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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Theorem: Geometry.SimplicialComplex.subfacet
Proof state before:
case neg.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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
obtain ⟨v, hv⟩ := h (face_dimension_le_space_dimension hu) htu hu
Proof state after:
case neg.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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
v : Finset E
hv : v ∈ K.facets ∧ u ⊆ v
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Theorem: Geometry.SimplicialComplex.subfacet
Proof state before:
case neg.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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∉ K.facets
u : Finset E
hu : u ∈ K.faces
htu : t ⊂ u
v : Finset E
hv : v ∈ K.facets ∧ u ⊆ v
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
exact ⟨v, hv.1, htu.1.trans hv.2⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.subfacet
Proof state before:
case pos
𝕜 : 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
hs : s ∈ K
t : Finset E
h : ∀ {t₂ : Finset E}, t₂.card ≤ FiniteDimensional.finrank 𝕜 E + 1 → t ⊂ t₂ → t₂ ∈ K → ∃ t ∈ K.facets, t₂ ⊆ t
ht : t ∈ K
htfacet : t ∈ K.facets
⊢ ∃ t_1 ∈ K.facets, t ⊆ t_1
Tactic:
exact ⟨t, htfacet, Subset.rfl⟩
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
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.facets = ∅ ↔ K = ⊥
Tactic:
refine' ⟨fun h => _, _⟩
Proof state after:
case refine'_1
𝕜 : 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
h : K.facets = ∅
⊢ K = ⊥

case refine'_2
𝕜 : 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 = ⊥ → K.facets = ∅
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_1
𝕜 : 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
h : K.facets = ∅
⊢ K = ⊥
Tactic:
ext s
Proof state after:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
⊢ s ∈ K.faces ↔ s ∈ ⊥.faces
Tactic:
refine' iff_of_false (fun hs => _) (Set.not_mem_empty _)
Proof state after:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
⊢ False
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_1.faces.h
𝕜 : 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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
⊢ False
Tactic:
obtain ⟨t, ht, -⟩ := subfacet hs
Proof state after:
case refine'_1.faces.h.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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ False
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_1.faces.h.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
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ False
Tactic:
exact h.subset ht
Proof state after:
no goals
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_2
𝕜 : 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 = ⊥ → K.facets = ∅
Tactic:
rintro rfl
Proof state after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ ⊥.facets = ∅
Theorem: Geometry.SimplicialComplex.facets_eq_empty_iff
Proof state before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
⊢ ⊥.facets = ∅
Tactic:
exact facets_bot
Proof state after:
no goals
Theorem: Finset.Colex.cons_le_cons
Proof state before:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
obtain rfl | hab := eq_or_ne a b
Proof state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Theorem: Finset.Colex.cons_le_cons
Proof state before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
classical
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
 singleton_le_singleton]
Proof state after:
no goals
Theorem: Finset.Colex.cons_le_cons
Proof state before:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a : α
ha hb : a ∉ s
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons a s hb } ↔ a ≤ a
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.Colex.cons_le_cons
Proof state before:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ { ofColex := cons a s ha } ≤ { ofColex := cons b s hb } ↔ a ≤ b
Tactic:
rw [← toColex_sdiff_le_toColex_sdiff', cons_sdiff_cons hab, cons_sdiff_cons hab.symm,
 singleton_le_singleton]
Proof state after:
no goals
Theorem: Finset.Colex.insert_le_insert
Proof state before:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
f : α → β
𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)
s t u : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∉ s
hb : b ∉ s
⊢ { ofColex := insert a s } ≤ { ofColex := insert b s } ↔ a ≤ b
Tactic:
rw [← cons_eq_insert _ _ ha, ← cons_eq_insert _ _ hb, cons_le_cons]
Proof state after:
no goals