affine independence help

Stream: maths

[Bhavik Mehta]

Here's the goal I'm stuck on:

import analysis.convex.basic
import linear_algebra.affine_space.independent

example {m : ℕ}
  (points : fin (m + 1) → fin (m + 1) → ℝ) -- We have (m+1) points in R^(m+1)
  (independent : affine_independent ℝ points) -- which are affinely independent
  (on_simplex : ∀ (x : fin (m + 1)), points x ∈ std_simplex (fin (m + 1)))
      -- and they're all on the standard (m+1)-simplex
  (h3 : ∀ (x : fin (m + 1)), points x 0 = 0) : -- and they all have x₀ = 0
  false := -- is a contradiction
begin

end

and I'm not really sure how to glue together the bits about affine spans and finite dimensional subspaces to solve it, any help?

[Joseph Myers]

It looks like you have two m-dimensional affine subspaces that contain the points (one containing std_simplex, one where the first coordinate is zero), so one approach would be to prove that their intersection is (m-1)-dimensional, at which point the results in linear_algebra.affine_space.finite_dimensional should be sufficient to finish things off. I suppose this means we need various lemmas about the dimension of an affine subspace given in some form by a single linear equation in coordinates (then some ad hoc argument to get the dimension of the intersection, e.g. via the dimension of the sup). (And coordinates should perhaps be considered generally in terms of an affine_equiv between the affine space and any ι → k with [fintype ι], with the case where the space is literally ι → k then being a special case of that.)

Rather than actually defining a notion of dimension (or findim) of an affine subspace we refer to the dimension of its direction (so avoiding duplicating lots of API for dimensions); the findim is a nat, which is generally convenient but does give the empty affine subspace dimension 0 not -1 which might mean you need a special case in the formal proof for m = 0.