Theorems · Definition · geometry

Affine.Simplex.interior

{k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → [PartialOrder k] → {n : ℕ} → Affine.Simplex k P n → Set P

The interior of a simplex is the set of points that can be expressed as an affine combination of the vertices with weights strictly between 0 and 1. This is equivalent to the intrinsic interior of the convex hull of the vertices.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic

Cited by

26 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddTorsorPartialOrder