mem_space_iff — Mathlib

English

Let K be a simplicial complex on E. A point x ∈ E lies in the space of K if and only if there exists a finite subset s of E which is a face of K such that x lies in the convex hull of s.

Русский

Пусть K — симплициальный комплекс над множеством E. Тогда точка x ∈ E принадлежит пространству K тогда и только тогда существует конечное множество s ⊆ E, являющееся гранью K, такое что x лежит в выпуклой оболочке множества s.

LaTeX

$$$x \\in K.space \\iff \\exists s \\in K.faces, x \\in convexHull 𝕜 (s : Set E)$$$

Lean4

theorem mem_space_iff : x ∈ K.space ↔ ∃ s ∈ K.faces, x ∈ convexHull 𝕜 (s : Set E) := by simp [space]

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