Zulip Chat Archive
Stream: general
Topic: Failed to synthesize ...
Heather Macbeth (May 24 2020 at 03:03):
What am I doing wrong here?
import analysis.normed_space.operator_norm
variables {𝕜 : Type*} [normed_field 𝕜]
variables {E : Type*} [normed_group E] [normed_space 𝕜 E]
variables {F : Type*} [normed_group F] [normed_space 𝕜 F]
variables {G : Type*} [normed_group G] [normed_space 𝕜 G]
#check E →L[𝕜] (F →L[𝕜] G)
gives the error "failed to synthesize type class instance for ... ⊢ topological_space (F →L[𝕜] G)
".
Heather Macbeth (May 24 2020 at 03:03):
I would have thought that Lean could infer a topological space structure on F →L[𝕜] G
, because (1) in analysis.normed_space.operator_norm
we have
instance to_normed_space : normed_space 𝕜 (E →L[𝕜] F)
(2) in analysis.normed_space.basic
we have, for [normed_space α E]
,
instance normed_space.topological_vector_space : topological_vector_space α E
(3) in topology.algebra.module
we have
abbreviation topological_vector_space (R : Type u) (M : Type v) [field R] [topological_space R]
[topological_space M] [add_comm_group M] [module R M]
Yury G. Kudryashov (May 24 2020 at 03:26):
Does to_normed_space
need a nondiscrete_normed_field
?
Heather Macbeth (May 24 2020 at 03:29):
Wow, I would never have caught that. Thank you, Yury!
Yury G. Kudryashov (May 24 2020 at 03:29):
BTW, could you please rename to_normed_space
in section normed_algebra
to normed_algebra.to_normed_space
?
Heather Macbeth (May 24 2020 at 03:31):
Sure.
Last updated: Dec 20 2023 at 11:08 UTC