Stream: Is there code for X?

Topic: Inner product space is metric space

Heather Macbeth (Dec 12 2020 at 20:22):

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 (Dec 12 2020 at 20:31):

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 (Dec 12 2020 at 20:45):

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

Heather Macbeth (Dec 12 2020 at 20:46):

Sebastien Gouezel said:

What happens if you include 𝕜?

This works, thank you!

Heather Macbeth (Dec 12 2020 at 20:46):

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 (Dec 12 2020 at 20:48):

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 (Dec 12 2020 at 20:50):

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!

Last updated: May 16 2021 at 05:21 UTC