Completeness of Rn

Stream: Is there code for X?

[Apurva Nakade]

Do we have a proof of the completeness of $R^n$?

The closest thing I found was docs#euclidean_space.inner_product_space

[Apurva Nakade]

(Why is the docs link not working? :thinking: )

[Yaël Dillies]

docs#Pi.complete ?

[Yaël Dillies]

Apurva Nakade said:

(Why is the docs link not working? :thinking: )

docs3#euclidean_space.inner_product_space

[Apurva Nakade]

Great, thanks! I was searching in the wrong file.

[Apurva Nakade]

Is there a simple way to have the following instance:

import Mathlib.Topology.UniformSpace.Pi
import Mathlib.Analysis.InnerProductSpace.PiL2


variable {n : Type*} [Fintype n]


instance : CompleteSpace (n → ℝ) := inferInstance
instance : CompleteSpace (EuclideanSpace ℝ n) := inferInstance

noncomputable instance : InnerProductSpace ℝ (EuclideanSpace ℝ n) := inferInstance
noncomputable instance : InnerProductSpace ℝ (n → ℝ) := inferInstance --error

[Apurva Nakade]

I can work with EuclideanSpace but simp doesn't like it much.

Nvm, I can make EuclideanSpace work.

[Yaël Dillies]

Not really, no. It would equip n → ℝ with the euclidean norm, and this conflicts with the infinity norm we have by default.

[Apurva Nakade]

Thanks again! I'll stick with EuclideanSpace then.