mem_face_iff — Mathlib

English

A d-simplex x belongs to the face S iff all its vertices lie in S.

Русский

d-мерный симплекс x принадлежит грани S тогда и только тогда, когда все её вершины лежат в S.

LaTeX

$$x ∈ (face S).obj d iff ∀ i : Fin(d+1), x i ∈ S$$

Lean4

@[simp]
theorem mem_face_iff {n : ℕ} (S : Finset (Fin (n + 1))) {d : ℕ} (x : (Δ[n] : SSet.{u}) _⦋d⦌) :
    x ∈ (face S).obj _ ↔ ∀ (i : Fin (d + 1)), x i ∈ S := by simp

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