Commit 2023-04-25 11:29 06aa02bb

View on Github →

feat: port Analysis.Convex.SimplicialComplex.Basic (#3643)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

added theorem Geometry.SimplicialComplex.convexHull_inter_convexHull

added theorem Geometry.SimplicialComplex.convexHull_subset_space

added theorem Geometry.SimplicialComplex.disjoint_or_exists_inter_eq_convexHull

added theorem Geometry.SimplicialComplex.face_subset_face_iff

added theorem Geometry.SimplicialComplex.faces_bot

added def Geometry.SimplicialComplex.facets

added theorem Geometry.SimplicialComplex.facets_bot

added theorem Geometry.SimplicialComplex.facets_subset

added theorem Geometry.SimplicialComplex.mem_facets

added theorem Geometry.SimplicialComplex.mem_space_iff

added theorem Geometry.SimplicialComplex.mem_vertices

added theorem Geometry.SimplicialComplex.not_facet_iff_subface

added def Geometry.SimplicialComplex.ofErase

added def Geometry.SimplicialComplex.ofSubcomplex

added def Geometry.SimplicialComplex.space

added theorem Geometry.SimplicialComplex.space_bot

added theorem Geometry.SimplicialComplex.vertex_mem_convexHull_iff

added def Geometry.SimplicialComplex.vertices

added theorem Geometry.SimplicialComplex.vertices_eq

added theorem Geometry.SimplicialComplex.vertices_subset_space

added structure Geometry.SimplicialComplex