19.1. General topological vector spaces
The following code adds a TVS called E with coefficients in the normed field 𝕜
to the Lean environment:
variable (E 𝕜 : Type*) [NormedField 𝕜]
[AddCommGroup E] [Module 𝕜 E]
[TopologicalSpace E]
[ContinuousAdd E] [ContinuousSMul 𝕜 E]
Since such a space is a topological group:
example : IsTopologicalAddGroup E :=
{ continuous_neg := E:Type u_1𝕜:Type u_2inst✝⁵:NormedField 𝕜inst✝⁴:AddCommGroup Einst✝³:Module 𝕜 Einst✝²:TopologicalSpace Einst✝¹:ContinuousAdd Einst✝:ContinuousSMul 𝕜 E⊢ Continuous fun a => -a
E:Type u_1𝕜:Type u_2inst✝⁵:NormedField 𝕜inst✝⁴:AddCommGroup Einst✝³:Module 𝕜 Einst✝²:TopologicalSpace Einst✝¹:ContinuousAdd Einst✝:ContinuousSMul 𝕜 Ex✝:E⊢ Neg.neg = HSMul.hSMul (-1)
E:Type u_1𝕜:Type u_2inst✝⁵:NormedField 𝕜inst✝⁴:AddCommGroup Einst✝³:Module 𝕜 Einst✝²:TopologicalSpace Einst✝¹:ContinuousAdd Einst✝:ContinuousSMul 𝕜 Ex✝¹:Ex✝:E⊢ -x✝ = -1 • x✝; All goals completed! 🐙 }
we could also assume IsTopologicalAddGroup instead of ContinuousAdd but
we usually make the superficially weaker assumption.