Inner product space is metric space

Stream: Is there code for X?

[Heather Macbeth]

Is there a way for typeclass inference to find the metric space structure on an inner product space? It doesn't seem to be the case at the moment:

import analysis.normed_space.inner_product

variables (𝕜 : Type*) [is_R_or_C 𝕜]
variables (E : Type*) [inner_product_space 𝕜 E]

-- works
example : normed_space 𝕜 E := by apply_instance

-- fails
example : metric_space E := by apply_instance

-- works
example : metric_space E := (inner_product_space.to_normed_group 𝕜).to_metric_space

The situation is as follows: docs#inner_product_space has a to_normed_group field, docs#normed_group has a to_metric_space field.

[Heather Macbeth]

Actually,

example : normed_group E := by apply_instance

fails as well. I can't see why the normed_group structure can't be found but the normed_space structure can be.

[Sebastien Gouezel]

What happens if you include 𝕜? Otherwise, your inner product space instance is probably not included in your examples.

[Heather Macbeth]

Sebastien Gouezel said:

What happens if you include 𝕜?

This works, thank you!

[Heather Macbeth]

Sebastien Gouezel said:

Otherwise, your inner product space instance is probably not included in your examples.

Could you explain this a little more?

[Sebastien Gouezel]

When you have variables and instances in scope, Lean does not include all of them in lemmas. For instance, if you have two variables a and b, and the statement of a lemma only involves a, then Lean will not make the lemma have the b variable. For instances, it only includes all the instances for which all the variables are present in the statement.

[Heather Macbeth]

Sebastien Gouezel said:

For instances, it only includes all the instances for which all the variables are present in the statement.

I didn't know this, but it makes perfect sense. Thank you!