instMembershipFinset — Mathlib

English

A Finset belongs to a simplicial complex if and only if it is a face of the complex.

Русский

Финисет принадлежит симплициальному комплексу тогда и только тогда, когда он является гранью комплекса.

LaTeX

$$$\text{Finset } s \in \text{SimplicialComplex } \mathcal{K} \quad\text{iff}\quad s \in \mathcal{K}.faces$$$

Lean4

/-- A `Finset` belongs to a `SimplicialComplex` if it's a face of it. -/
instance : Membership (Finset E) (SimplicialComplex 𝕜 E) :=
  ⟨fun K s => s ∈ K.faces⟩

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