Creating values in EuclideanSpace

Stream: new members

[Dominic Steinitz]

I naively thought that

def x := (![1, 0] : EuclideanSpace ℝ (Fin 2))

would create a value of EuclideanSpace ℝ (Fin 2) but the type shown on x is x : Fin (Nat.succ 1) → ℝ so after a bit more searching I found

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html#EuclideanSpace

But if I try this

noncomputable
def q := (!₂[1, 0] : EuclideanSpace ℝ (Fin 2))

I see the type of q is q : WithLp 2 (Fin 2 → ℝ).

So how do I get a type of EuclideanSpace ℝ (Fin 2)?

[Eric Wieser]

EuclideanSpace is an abbreviation for WithLp, so the !₂ spelling is fine and it really is of the type you want

[Robin Arnez]

def x := (![1, 0] : EuclideanSpace ℝ (Fin 2)) creates a term of a type that's definitionally equivalent to what you want (EuclideanSpace ℝ (Fin 2)), if you want to make it stricter you can do show EuclideanSpace ℝ (Fin 2) from ![1, 0] which should give you the right one but perhaps you'd rather want to use !₂ to avoid defeq abuse.

[Eric Wieser]

What you care about is whether it's reducibly definitionally equal, which the ![ spelling is not

[Eric Wieser]

You will find that none of the theorems work the way you want to if you use that incorrect spelling.