feat(linear_algebra/affine_space/barycentric_coords): barycentric coo…

…rdinates are 1 in zero dimensions (#9564)

src/data/set/basic.lean

@@ -1582,6 +1582,12 @@ by { rcases hs.eq_empty_or_singleton with rfl|⟨x, rfl⟩, exacts [he, h₁ _]
 lemma subsingleton_univ [subsingleton α] : (univ : set α).subsingleton :=
 λ x hx y hy, subsingleton.elim x y
 
+lemma subsingleton_of_univ_subsingleton (h : (univ : set α).subsingleton) : subsingleton α :=
+⟨λ a b, h (mem_univ a) (mem_univ b)⟩
+
+@[simp] lemma subsingleton_univ_iff : (univ : set α).subsingleton ↔ subsingleton α :=
+⟨subsingleton_of_univ_subsingleton, λ h, @subsingleton_univ _ h⟩
+
 lemma subsingleton_of_subsingleton [subsingleton α] {s : set α} : set.subsingleton s :=
 subsingleton.mono subsingleton_univ (subset_univ s)
 

src/linear_algebra/affine_space/affine_subspace.lean

@@ -700,6 +700,16 @@ by rw [direction_eq_vector_span, bot_coe, vector_span_def, vsub_empty, submodule
 
 variables {k V P}
 
+lemma subsingleton_of_subsingleton_span_eq_top {s : set P} (h₁ : s.subsingleton)
+  (h₂ : affine_span k s = ⊤) : subsingleton P :=
+begin
+  obtain ⟨p, hp⟩ := affine_subspace.nonempty_of_affine_span_eq_top k V P h₂,
+  have : s = {p}, { exact subset.antisymm (λ q hq, h₁ hq hp) (by simp [hp]), },
+  rw [this, ← affine_subspace.ext_iff, affine_subspace.coe_affine_span_singleton,
+    affine_subspace.top_coe, eq_comm, ← subsingleton_iff_singleton (mem_univ _)] at h₂,
+  exact subsingleton_of_univ_subsingleton h₂,
+end
+
 /-- A nonempty affine subspace is `⊤` if and only if its direction is
 `⊤`. -/
 @[simp] lemma direction_eq_top_iff_of_nonempty {s : affine_subspace k P}

src/linear_algebra/affine_space/barycentric_coords.lean

@@ -107,3 +107,19 @@ begin
   simp only [barycentric_coord_apply, hi, finset.affine_combination_eq_linear_combination, if_false,
     hw, mul_boole, function.comp_app, smul_eq_mul, s.sum_ite_eq, s.map_affine_combination p w hw],
 end
+
+@[simp] lemma coe_barycentric_coord_of_subsingleton_eq_one [subsingleton ι] (i : ι) :
+  (barycentric_coord h_ind h_tot i : P → k) = 1 :=
+begin
+  ext q,
+  have hp : (range p).subsingleton,
+  { rw ← image_univ,
+    apply subsingleton.image,
+    apply subsingleton_of_subsingleton, },
+  haveI := affine_subspace.subsingleton_of_subsingleton_span_eq_top hp h_tot,
+  let s : finset ι := {i},
+  have hi : i ∈ s, { simp, },
+  have hw : s.sum (function.const ι (1 : k)) = 1, { simp, },
+  have hq : q = s.affine_combination p (function.const ι (1 : k)), { simp, },
+  rw [pi.one_apply, hq, barycentric_coord_apply_combination_of_mem h_ind h_tot hi hw],
+end