Cartesian product

Stream: new members

[Maxime Darrin]

Hi is there a way to talk about \R^2, \R^3, ... and to get tuples such that
v : \R^4, v[0] + v[1] + v[2] = v[3] for example ?

[Anne Baanen]

ℝ⁴ is written fin 4 → ℝ, for example:

[Anne Baanen]

import data.matrix.notation
import data.real.basic

def v : fin 4 → ℝ := ![1, 2, 3, 4]

example : ∀ v : fin 4 → ℝ, v = ![v 0, v 1, v 2, v 3] :=
begin
  intro v,
  ext i,
  fin_cases i; simp
end

[Anne Baanen]

And your example property looks like:

def last_eq_sum_first (v : fin 4 → ℝ) :=
v 0 + v 1 + v 2 = v 3