## Stream: math-comp analysis

### Topic: Using natmul_continuous on the support realType

#### Yves Bertot (Jun 01 2021 at 06:23):

I am working on an exercise proof that x |-> 2 * x is continuous. the statement I write is as follows:

``````Lemma times2_continuous : continuous (fun w : R => 2%:R * w).
``````

I found that there exists a theorem called `natmul_continuous`, so I decide to prove the intermediate statement:

``````have ctn : continuous (fun w : R => w *+ 2).
exact: (@natmul_continuous _ (normedtype.numFieldNormedType.real_normedModType R))
``````

I am really puzzled that I had to produce the `normedModType` for R by hand in this unsightly manner.

#### Yves Bertot (Jun 01 2021 at 06:28):

I should have said that `R : realType` in this context.

#### Laurent Théry (Jun 01 2021 at 06:40):

You must have the wrong import. Your example works in my setting.

#### Laurent Théry (Jun 01 2021 at 06:42):

``````From mathcomp Require Import matrix interval rat.
Require Import boolp reals ereal.
Require Import classical_sets posnum topology normedtype landau sequences.
Require Import derive.

Import Order.TTheory GRing.Theory Num.Def  Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope ring_scope.

Lemma ctn (R : realType) : continuous (fun w : R => w *+ 2).
exact: natmul_continuous.
Qed.
``````

works with me

#### Yves Bertot (Jun 01 2021 at 06:45):

Thansk, this solves my problem in the short term. How do you make sure to have the right sequence of imports?

#### Laurent Théry (Jun 01 2021 at 06:48):

I just copy and paste headers :flushed:

Where from?

from here

Thanks

#### Notification Bot (Jun 01 2021 at 10:08):

This topic was moved here from #math-comp users > Using natmul_continuous on the support realType by Cyril Cohen

Last updated: Apr 14 2024 at 09:39 UTC