hasBot — Mathlib

English

The bottom simplicial complex has no faces, hence its vertex set is empty.

Русский

Нижний симплилический комплекс не имеет граней, следовательно, его множество вершин пустое.

LaTeX

$$(\\bot : SimplicialComplex 𝕜 E).vertices = ∅$$

Lean4

instance hasBot : Bot (SimplicialComplex 𝕜 E) :=
  ⟨{  faces := ∅
      empty_notMem := Set.notMem_empty ∅
      indep := fun hs => (Set.notMem_empty _ hs).elim
      down_closed := fun hs => (Set.notMem_empty _ hs).elim
      inter_subset_convexHull := fun hs => (Set.notMem_empty _ hs).elim }⟩

Похожие утверждения