subset_space — Mathlib

English

If s is a finite set forming a face of K, then the underlying set of s is contained in the space of K.

Русский

Если s образует грань K, то множество, соответствующее s, содержится в пространстве K.

LaTeX

$$$s \\in K.faces \\Rightarrow (s : Set E) \\subseteq K.space$$$

Lean4

protected theorem subset_space (hs : s ∈ K.faces) : (s : Set E) ⊆ K.space :=
  (subset_convexHull 𝕜 _).trans <| convexHull_subset_space hs

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