mem_affineSpan_range_face_points_iff

English

Deprecated variant: for a simplex s and fs with |fs| = m+1, a vertex s.points i lies in the affine span of the range of the face points if and only if i ∈ fs.

Русский

Устаревший вариант: для симплекса s и fs с |fs| = m+1, вершина s.points i лежит в афинном обобщении образа точек грани тогда, когда i ∈ fs.

LaTeX

$$$ s.points(i) \\in \\operatorname{affineSpan}_k( \\operatorname{range}((s.face(h)).points) ) \\iff i \\in fs $$$

Lean4

@[deprecated mem_affineSpan_image_iff (since := "2025-05-18")]
theorem mem_affineSpan_range_face_points_iff [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))}
    {m : ℕ} (h : #fs = m + 1) {i : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs := by
  simp

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