Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 23:34 c3391c26

View on Github →

feat(analysis/convex/simplicial_complex): Simplicial complexes (#9762) This introduces simplicial complexes in modules.

Estimated changes

Created src/analysis/convex/simplicial_complex/basic.lean

added theorem geometry.simplicial_complex.convex_hull_inter_convex_hull

added theorem geometry.simplicial_complex.convex_hull_subset_space

added theorem geometry.simplicial_complex.disjoint_or_exists_inter_eq_convex_hull

added theorem geometry.simplicial_complex.face_subset_face_iff

added theorem geometry.simplicial_complex.faces_bot

added def geometry.simplicial_complex.facets

added theorem geometry.simplicial_complex.facets_bot

added theorem geometry.simplicial_complex.facets_subset

added theorem geometry.simplicial_complex.mem_facets

added theorem geometry.simplicial_complex.mem_space_iff

added theorem geometry.simplicial_complex.mem_vertices

added theorem geometry.simplicial_complex.not_facet_iff_subface

added def geometry.simplicial_complex.of_erase

added def geometry.simplicial_complex.of_subcomplex

added def geometry.simplicial_complex.space

added theorem geometry.simplicial_complex.space_bot

added theorem geometry.simplicial_complex.vertex_mem_convex_hull_iff

added def geometry.simplicial_complex.vertices

added theorem geometry.simplicial_complex.vertices_eq

added theorem geometry.simplicial_complex.vertices_subset_space

added structure geometry.simplicial_complex