Documentation

@[reducible, inline]

abbrev Affine.Triangle (k : Type u_1) {V : Type u_2} (P : Type u_5) [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :

Type u_5

A Triangle k P is a collection of three affinely independent points.

Instances For

def Affine.Simplex.mkOfPoint (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) :

Simplex k P 0

Construct a 0-simplex from a point.

Instances For

@[simp]

theorem Affine.Simplex.mkOfPoint_points (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) (i : Fin 1) :

(mkOfPoint k p).points i = p

The point in a simplex constructed with mkOfPoint.

@[implicit_reducible]

instance Affine.Simplex.instInhabitedOfNatNat (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Inhabited P] :

Inhabited (Simplex k P 0)

instance Affine.Simplex.nonempty (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] :

Nonempty (Simplex k P 0)

@[simp]

theorem Affine.Simplex.range_mkOfPoint_points (k : Type u_1) {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (p : P) :

Set.range (mkOfPoint k p).points = {p}

The set of points in a simplex constructed with mkOfPoint.

theorem Affine.Simplex.ext {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s1 s2 : Simplex k P n} (h : ∀ (i : Fin (n + 1)), s1.points i = s2.points i) :

s1 = s2

Two simplices are equal if they have the same points.

theorem Affine.Simplex.ext_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} {s1 s2 : Simplex k P n} :

s1 = s2 ↔ ∀ (i : Fin (n + 1)), s1.points i = s2.points i

Two simplices are equal if and only if they have the same points.

def Affine.Simplex.face {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

Simplex k P m

A face of a simplex is a simplex with the given subset of points.

Instances For

theorem Affine.Simplex.face_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) (i : Fin (m + 1)) :

(s.face h).points i = s.points ((fs.orderEmbOfFin h) i)

The points of a face of a simplex are given by mono_of_fin.

theorem Affine.Simplex.face_points' {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

(s.face h).points = s.points ∘ ⇑(fs.orderEmbOfFin h)

The points of a face of a simplex are given by mono_of_fin.

@[simp]

theorem Affine.Simplex.face_eq_mkOfPoint {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :

s.face ⋯ = mkOfPoint k (s.points i)

A single-point face equals the 0-simplex constructed with mkOfPoint.

@[simp]

theorem Affine.Simplex.range_face_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

Set.range (s.face h).points = s.points '' ↑fs

The set of points of a face.

theorem Affine.Simplex.affineSpan_face_le {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

affineSpan k (Set.range (s.face h).points) ≤ affineSpan k (Set.range s.points)

theorem Affine.Simplex.points_mem_affineSpan_face {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {i : Fin (n + 1)} :

s.points i ∈ affineSpan k (Set.range (s.face h).points) ↔ i ∈ fs

def Affine.Simplex.faceOpposite {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :

Simplex k P (n - 1)

The face of a simplex with all but one point.

Instances For

@[simp]

theorem Affine.Simplex.range_faceOpposite_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :

Set.range (s.faceOpposite i).points = s.points '' {i}ᶜ

theorem Affine.Simplex.affineSpan_faceOpposite_le {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :

affineSpan k (Set.range (s.faceOpposite i).points) ≤ affineSpan k (Set.range s.points)

theorem Affine.Simplex.points_mem_affineSpan_faceOpposite {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} [NeZero n] (s : Simplex k P n) {i j : Fin (n + 1)} :

s.points j ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ j ≠ i

theorem Affine.Simplex.points_notMem_affineSpan_faceOpposite {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) :

s.points i ∉ affineSpan k (Set.range (s.faceOpposite i).points)

theorem Affine.Simplex.faceOpposite_point_eq_point_succAbove {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) (i : Fin (n + 1)) (j : Fin (n - 1 + 1)) :

(s.faceOpposite i).points j = s.points (i.succAbove (Fin.cast ⋯ j))

theorem Affine.Simplex.faceOpposite_point_eq_point_rev {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (i : Fin 2) (n : Fin 1) :

(s.faceOpposite i).points n = s.points i.rev

@[simp]

theorem Affine.Simplex.faceOpposite_point_eq_point_one {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (n : Fin 1) :

(s.faceOpposite 0).points n = s.points 1

@[simp]

theorem Affine.Simplex.faceOpposite_point_eq_point_zero {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (s : Simplex k P 1) (n : Fin 1) :

(s.faceOpposite 1).points n = s.points 0

instance Affine.Simplex.instNonemptyElemComplSetSingletonOfNontrivial {α : Type u_8} [Nontrivial α] (i : α) :

Nonempty ↑{i}ᶜ

Needed to make affineSpan (s.points '' {i}ᶜ) nonempty.

@[simp]

theorem Affine.Simplex.mem_affineSpan_image_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [Nontrivial k] {n : ℕ} (s : Simplex k P n) {fs : Set (Fin (n + 1))} {i : Fin (n + 1)} :

s.points i ∈ affineSpan k (s.points '' fs) ↔ i ∈ fs

theorem Affine.Simplex.affineCombination_mem_affineSpan_faceOpposite_iff {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) {i : Fin (n + 1)} :

(Finset.affineCombination k Finset.univ s.points) w ∈ affineSpan k (Set.range (s.faceOpposite i).points) ↔ w i = 0

def Affine.Simplex.map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) :

Simplex k P₂ n

Push forward an affine simplex under an injective affine map.

Instances For

@[simp]

theorem Affine.Simplex.map_points {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) :

(s.map f hf).points = ⇑f ∘ s.points

@[simp]

theorem Affine.Simplex.map_id {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) :

s.map (AffineMap.id k P) ⋯ = s

theorem Affine.Simplex.map_comp {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {V₃ : Type u_4} {P : Type u_5} {P₂ : Type u_6} {P₃ : Type u_7} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [AddCommGroup V₃] [Module k V] [Module k V₂] [Module k V₃] [AddTorsor V P] [AddTorsor V₂ P₂] [AddTorsor V₃ P₃] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (g : P₂ →ᵃ[k] P₃) (hg : Function.Injective ⇑g) :

s.map (g.comp f) ⋯ = (s.map f hf).map g hg

@[simp]

theorem Affine.Simplex.face_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

(s.map f hf).face h = (s.face h).map f hf

@[simp]

theorem Affine.Simplex.faceOpposite_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} [NeZero n] (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (i : Fin (n + 1)) :

(s.map f hf).faceOpposite i = (s.faceOpposite i).map f hf

@[simp]

theorem Affine.Simplex.map_mkOfPoint {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (p : P) :

(mkOfPoint k p).map f hf = mkOfPoint k (f p)

def Affine.Simplex.reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :

Simplex k P n

Remap a simplex along an Equiv of index types.

Instances For

@[simp]

theorem Affine.Simplex.reindex_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (a✝ : Fin (n + 1)) :

(s.reindex e).points a✝ = (s.points ∘ ⇑e.symm) a✝

@[simp]

theorem Affine.Simplex.reindex_refl {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) :

s.reindex (Equiv.refl (Fin (n + 1))) = s

Reindexing by Equiv.refl yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_trans {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n₁ n₂ n₃ : ℕ} (e₁₂ : Fin (n₁ + 1) ≃ Fin (n₂ + 1)) (e₂₃ : Fin (n₂ + 1) ≃ Fin (n₃ + 1)) (s : Simplex k P n₁) :

s.reindex (e₁₂.trans e₂₃) = (s.reindex e₁₂).reindex e₂₃

Reindexing by the composition of two equivalences is the same as reindexing twice.

@[simp]

theorem Affine.Simplex.reindex_reindex_symm {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :

(s.reindex e).reindex e.symm = s

Reindexing by an equivalence and its inverse yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_symm_reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (n + 1) ≃ Fin (m + 1)) :

(s.reindex e.symm).reindex e = s

Reindexing by the inverse of an equivalence and that equivalence yields the original simplex.

@[simp]

theorem Affine.Simplex.reindex_range_points {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :

Set.range (s.reindex e).points = Set.range s.points

Reindexing a simplex produces one with the same set of points.

theorem Affine.Simplex.reindex_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) :

(s.map f hf).reindex e = (s.reindex e).map f hf

theorem Affine.Simplex.range_face_reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) {fs : Finset (Fin (n + 1))} {n' : ℕ} (h : fs.card = n' + 1) :

Set.range ((s.reindex e).face h).points = Set.range (s.face ⋯).points

theorem Affine.Simplex.range_faceOpposite_reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} [NeZero m] [NeZero n] (s : Simplex k P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (i : Fin (n + 1)) :

Set.range ((s.reindex e).faceOpposite i).points = Set.range (s.faceOpposite (e.symm i)).points

def Affine.Simplex.restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) :

Simplex k (↥S) n

Restrict an affine simplex to an affine subspace that contains it.

Instances For

@[simp]

theorem Affine.Simplex.restrict_points_coe {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S : AffineSubspace k P) (hS : affineSpan k (Set.range s.points) ≤ S) (i : Fin (n + 1)) :

↑((s.restrict S hS).points i) = s.points i

@[simp]

theorem Affine.Simplex.restrict_map_inclusion {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) (S₁ S₂ : AffineSubspace k P) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hS₂ : S₁ ≤ S₂) :

(s.restrict S₁ hS₁).map (AffineSubspace.inclusion hS₂) ⋯ = s.restrict S₂ ⋯

Restricting to S₁ then mapping to a larger S₂ is the same as restricting to S₂.

@[simp]

theorem Affine.Simplex.map_subtype_restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (S : AffineSubspace k P) [Nonempty ↥S] (s : Simplex k (↥S) n) :

(s.map S.subtype ⋯).restrict S ⋯ = s

theorem Affine.Simplex.restrict_map_restrict {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V] [AddCommGroup V₂] [Module k V] [Module k V₂] [AddTorsor V P] [AddTorsor V₂ P₂] {n : ℕ} (s : Simplex k P n) (f : P →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (S₁ : AffineSubspace k P) (S₂ : AffineSubspace k P₂) (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hfS : AffineSubspace.map f S₁ ≤ S₂) :

(s.restrict S₁ hS₁).map (f.restrict hfS) ⋯ = (s.map f hf).restrict S₂ ⋯

Restricting to S₁ then mapping through the restriction of f to S₁ →ᵃ[k] S₂ is the same as mapping through unrestricted f, then restricting to S₂.

@[simp]

theorem Affine.Simplex.restrict_map_subtype {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) :

(s.restrict (affineSpan k (Set.range s.points)) ⋯).map (affineSpan k (Set.range s.points)).subtype ⋯ = s

Restricting to affineSpan k (Set.range s.points) can be reversed by mapping through AffineSubspace.subtype.

theorem Affine.Simplex.restrict_reindex {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {m n : ℕ} (s : Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) {S : AffineSubspace k P} (hS : affineSpan k (Set.range s.points) ≤ S) :

(s.reindex e).restrict S ⋯ = (s.restrict S hS).reindex e

theorem Affine.Simplex.face_restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} (s : Simplex k P n) {S : AffineSubspace k P} (hS : affineSpan k (Set.range s.points) ≤ S) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) :

(s.restrict S hS).face h = (s.face h).restrict S ⋯

theorem Affine.Simplex.faceOpposite_restrict {k : Type u_1} {V : Type u_2} {P : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {n : ℕ} [NeZero n] (s : Simplex k P n) {S : AffineSubspace k P} (hS : affineSpan k (Set.range s.points) ≤ S) (i : Fin (n + 1)) :

(s.restrict S hS).faceOpposite i = (s.faceOpposite i).restrict S ⋯

def Affine.Simplex.setInterior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (I : Set k) {n : ℕ} (s : 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 in a set I.

Instances For

theorem Affine.Simplex.affineCombination_mem_setInterior_iff {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {I : Set k} {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ Simplex.setInterior I s ↔ ∀ (i : Fin (n + 1)), w i ∈ I

@[simp]

theorem Affine.Simplex.setInterior_reindex {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (I : Set k) {m n : ℕ} (s : Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) :

Simplex.setInterior I (s.reindex e) = Simplex.setInterior I s

theorem Affine.Simplex.setInterior_mono {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {I J : Set k} (hij : I ⊆ J) {n : ℕ} (s : Simplex k P n) :

Simplex.setInterior I s ⊆ Simplex.setInterior J s

theorem Affine.Simplex.setInterior_subset_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] {I : Set k} {n : ℕ} {s : Simplex k P n} :

Simplex.setInterior I s ⊆ ↑(affineSpan k (Set.range s.points))

theorem Affine.Simplex.setInterior_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (I : Set k) {n : ℕ} (s : Simplex k P n) {f : P →ᵃ[k] P₂} (hf : Function.Injective ⇑f) :

Simplex.setInterior I (s.map f hf) = ⇑f '' Simplex.setInterior I s

theorem Affine.Simplex.setInterior_restrict {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (I : Set k) {n : ℕ} (s : Simplex k P n) {S : AffineSubspace k P} (hS : affineSpan k (Set.range s.points) ≤ S) :

Simplex.setInterior I (s.restrict S hS) = ⇑S.subtype ⁻¹' Simplex.setInterior I s

def Affine.Simplex.interior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : 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.

Instances For

@[simp]

theorem Affine.Simplex.interior_reindex {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {m n : ℕ} (s : Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) :

(s.reindex e).interior = s.interior

theorem Affine.Simplex.affineCombination_mem_interior_iff {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ s.interior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1

def Affine.Simplex.closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) :

Set P

s.closedInterior is the set of points that can be expressed as an affine combination of the vertices with weights between 0 and 1 inclusive. This is equivalent to the convex hull of the vertices or the closure of the interior.

Instances For

@[simp]

theorem Affine.Simplex.closedInterior_reindex {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {m n : ℕ} (s : Simplex k P n) (e : Fin (n + 1) ≃ Fin (m + 1)) :

(s.reindex e).closedInterior = s.closedInterior

theorem Affine.Simplex.affineCombination_mem_closedInterior_iff {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} {s : Simplex k P n} {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ s.closedInterior ↔ ∀ (i : Fin (n + 1)), w i ∈ Set.Icc 0 1

theorem Affine.Simplex.interior_subset_closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) :

s.interior ⊆ s.closedInterior

theorem Affine.Simplex.point_notMem_interior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :

s.points i ∉ s.interior

theorem Affine.Simplex.point_mem_closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Simplex k P n) (i : Fin (n + 1)) :

s.points i ∈ s.closedInterior

theorem Affine.Simplex.interior_ssubset_closedInterior {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [ZeroLEOneClass k] {n : ℕ} (s : Simplex k P n) :

s.interior ⊂ s.closedInterior

theorem Affine.Simplex.closedInterior_subset_affineSpan {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} {s : Simplex k P n} :

s.closedInterior ⊆ ↑(affineSpan k (Set.range s.points))

@[simp]

theorem Affine.Simplex.interior_eq_empty {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] (s : Simplex k P 0) :

s.interior = ∅

@[simp]

theorem Affine.Simplex.closedInterior_eq_singleton {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [ZeroLEOneClass k] (s : Simplex k P 0) :

s.closedInterior = {s.points 0}

theorem Affine.Simplex.affineCombination_mem_setInterior_face_iff_mem {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] (I : Set k) {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ Simplex.setInterior I (s.face h) ↔ (∀ i ∈ fs, w i ∈ I) ∧ ∀ i ∉ fs, w i = 0

theorem Affine.Simplex.affineCombination_mem_interior_face_iff_mem_Ioo {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).interior ↔ (∀ i ∈ fs, w i ∈ Set.Ioo 0 1) ∧ ∀ i ∉ fs, w i = 0

theorem Affine.Simplex.affineCombination_mem_closedInterior_face_iff_mem_Icc {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).closedInterior ↔ (∀ i ∈ fs, w i ∈ Set.Icc 0 1) ∧ ∀ i ∉ fs, w i = 0

theorem Affine.Simplex.affineCombination_mem_interior_face_iff_pos {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [IsOrderedAddMonoid k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} [NeZero m] (h : fs.card = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).interior ↔ (∀ i ∈ fs, 0 < w i) ∧ ∀ i ∉ fs, w i = 0

theorem Affine.Simplex.affineCombination_mem_closedInterior_face_iff_nonneg {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] [IsOrderedAddMonoid k] {n : ℕ} (s : Simplex k P n) {fs : Finset (Fin (n + 1))} {m : ℕ} (h : fs.card = m + 1) {w : Fin (n + 1) → k} (hw : ∑ i : Fin (n + 1), w i = 1) :

(Finset.affineCombination k Finset.univ s.points) w ∈ (s.face h).closedInterior ↔ (∀ i ∈ fs, 0 ≤ w i) ∧ ∀ i ∉ fs, w i = 0

theorem Affine.Simplex.interior_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [PartialOrder k] {n : ℕ} (s : Simplex k P n) {f : P →ᵃ[k] P₂} (hf : Function.Injective ⇑f) :

(s.map f hf).interior = ⇑f '' s.interior

theorem Affine.Simplex.closedInterior_map {k : Type u_1} {V : Type u_2} {V₂ : Type u_3} {P : Type u_4} {P₂ : Type u_5} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [PartialOrder k] {n : ℕ} (s : Simplex k P n) {f : P →ᵃ[k] P₂} (hf : Function.Injective ⇑f) :

(s.map f hf).closedInterior = ⇑f '' s.closedInterior

theorem Affine.Simplex.interior_restrict {k : Type u_1} {V : Type u_2} {P : Type u_4} [Ring k] [AddCommGroup V] [Module k V] [AddTorsor V P] [PartialOrder k] {n : ℕ} (s : Simplex k P n) {S : AffineSubspace k P} (hS : affineSpan k (Set.range s.points) ≤ S) :

(s.restrict S hS).interior = ⇑S.subtype ⁻¹' s.interior