Def Geometry.SimplicialComplex.ofErase

Modification history

2023-04-25 11:29

Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean

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

Added Geometry.SimplicialComplex.ofErase View on Github →