Theorems · Theorem · convex and discrete geometry

Geometry.SimplicialComplex.ext

∀ {𝕜 : Type u_1} {E : Type u_2} {inst : Ring 𝕜} {inst_1 : PartialOrder 𝕜} {inst_2 : AddCommGroup E}
  {inst_3 : Module 𝕜 E} {x y : Geometry.SimplicialComplex 𝕜 E}, x.faces = y.faces → x = y

Defined in

Mathlib.Analysis.Convex.SimplicialComplex.Basic

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound