A simple equivalence between topological vector spaces

Stream: new members

[Michiel Huttener]

I would like to show

$$C((-1,1);\mathbb{R} ) \times \mathbb{R} \cong C^1((-1,1);\mathbb{R} ) ,$$

but I don't know how to state it :upside_down:
(the equivalence is as topological vector spaces)

Some questions:

1. Set.Ioo : is there notation for (-1,1), similar to [[-1,1]] for [-1,1]?
2. I found ContinuousMap for the type of continuous functions (between given topological spaces), but is it already a topological module? I could not find an instance.
3. What is the type of continuously differentiable functions?

[Yaël Dillies]

1. No. (-1, 1) would be terrible notation and ]-1, 1[ sadly confuses Lean
2. Yes. Sorry about the name, but it is around docs#ContinuousMap.instTopologicalAddGroupContinuousMapCompactOpenInstAddGroupContinuousMapToAddGroup
3. It is docs#ContDiff

[Michiel Huttener]

Thanks! I also found 3, but this is a Prop. How would I use it as a type?
Also, is there a better way to find instances than just browsing Mathlib or guessing their name? Something like "import all of Mathlib and if you've found something, tell me where"?

[Alex J. Best]

There are many such things (tactics like exact? apply?, there is also the #synth command to syntheise instances and #find command or https://loogle.lean-lang.org/), if you say more specifcally (with an example!) what sort of input you want to give and what output you would want we can guide you more

[Michiel Huttener]

Below is a MWE.
I defined a type for continuously differentiable functions and will have to show a lot of instances.
(Note that I changed the goal a bit: (-1,1) is now ℝ.)
Is this the/a way to go?

import Mathlib.Topology.ContinuousFunction.Algebra
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.ContDiff.Basic

-- continuously differentiable maps
structure ContDiffMap (n : ℕ) where
  toFun : ℝ → ℝ
  contDiff_toFun : ContDiff ℝ n toFun

instance (n : ℕ) : CoeFun (ContDiffMap n) (fun _ => ℝ → ℝ) where
  coe m := m.toFun

instance (n : ℕ) : SMul ℝ (ContDiffMap n) where
  smul s f := sorry

instance (n : ℕ) : AddCommGroup (ContDiffMap n) where
  add := sorry
  add_assoc := sorry
  zero := sorry
  zero_add := sorry
  add_zero := sorry
  neg := sorry
  add_left_neg := sorry
  add_comm := sorry

instance (n : ℕ) : Module ℝ (ContDiffMap n) where
  one_smul := sorry
  mul_smul := sorry
  smul_zero := sorry
  smul_add := sorry
  add_smul := sorry
  zero_smul := sorry

instance (n : ℕ) : TopologicalSpace (ContDiffMap n) where
  IsOpen := sorry
  isOpen_inter := sorry
  isOpen_sUnion := sorry
  isOpen_univ := sorry

instance (n : ℕ) : ContinuousSMul ℝ (ContDiffMap n) where
  continuous_smul := sorry

instance (n : ℕ) : TopologicalAddGroup (ContDiffMap n) where
  continuous_add := sorry
  continuous_neg := sorry

-- Fundamental theorem of calculus
def iso : (C(ℝ, ℝ) × ℝ) ≃L[ℝ] (ContDiffMap 1) := by
  sorry

[Michiel Huttener]

Also, is there a way to let vscode complete the necessary fields while defining an instance?

[Kevin Buzzard]

The problem with the answer we have for VS Code completing necessary fields is that it's instance foo : MyClass := _ and then put your cursor next to the _ and then click on the blue bulb and then click on the option which mentions fields of a structure, and it prints out many fields which don't necessarily need to be filled in because they are filled in automatically. But in your situation maybe this is not a problem (in algebra it's a big problem because beginners don't have a clue what nsmul is).

[Kevin Buzzard]

When I'm in this situation I usually just fill in the fields one by one and look at the error to tell me the name of the next field :-)

[Mario Carneiro]

@Kevin Buzzard Fixed in std4#577