mem_affineSpan_range_faceOpposite_points_iff

English

Similarly, for opposite faces, a vertex lies in the affine span of the opposite-face points precisely when the indices are not equal.

Русский

Аналогично для противоположных граней: вершина лежит в афинном обобщении точек противоположной грани тогда, когда индексы не совпадают.

LaTeX

$$$ s.points(i) \\in \\operatorname{affineSpan}_k( \\operatorname{range}((s.faceOpposite j).points) ) \\iff i \\neq j $$$

Lean4

@[deprecated mem_affineSpan_image_iff (since := "2025-05-18")]
theorem mem_affineSpan_range_faceOpposite_points_iff [Nontrivial k] {n : ℕ} [NeZero n] (s : Simplex k P n)
    {i j : Fin (n + 1)} : s.points i ∈ affineSpan k (Set.range (s.faceOpposite j).points) ↔ i ≠ j := by simp

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