Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull
theorem Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
{K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
s ∈ K.faces →
t ∈ K.faces →
Disjoint ((convexHull 𝕜) ↑s) ((convexHull 𝕜) ↑t) ∨
∃ u ∈ K.faces, (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) ↑u
This theorem in Geometry pertains to a simplicial complex. The theorem states that for any ordered ring `𝕜`, any additive commutative group `E`, any module `E` over `𝕜`, any simplicial complex `K` and any two finite sets `s` and `t` of `E`, if `s` and `t` are faces in `K`, then either the convex hulls of `s` and `t` (in the vector space sense) are disjoint (meaning that their infimum is the bottom element in the lattice of subsets of `E`), or there exists a face `u` in `K` such that the intersection of the convex hulls of `s` and `t` is equal to the convex hull of `u`. In simpler terms, either the convex hulls of two faces in a simplicial complex do not overlap, or the overlap forms the convex hull of another face in the complex.
More concisely: For any simplicial complex and any two faces, the convex hulls of these faces either do not overlap or intersect in the convex hull of another face.
|
Geometry.SimplicialComplex.face_subset_face_iff
theorem Geometry.SimplicialComplex.face_subset_face_iff :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : OrderedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
{K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
s ∈ K.faces → t ∈ K.faces → ((convexHull 𝕜) ↑s ⊆ (convexHull 𝕜) ↑t ↔ s ⊆ t)
This theorem states that for any ordered ring `𝕜`, any additively commutative group `E`, and any `𝕜`-module `E`, given a simplicial complex `K` over `𝕜` and `E`, and two finite sets `s` and `t` of `E`, if `s` and `t` are faces of the simplicial complex `K`, then the convex hull of `s` is a subset of the convex hull of `t` if and only if `s` itself is a subset of `t`. This implies that in the context of a simplicial complex, one face is a subset of another face precisely when all the vertices of the first face are also vertices of the second face.
More concisely: In the context of a simplicial complex over an ordered ring and an additively commutative group, the convex hull of one face is a subset of the convex hull of another face if and only if the first face is a subset of the second face.
|