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:

Yves Bertot (Jun 01 2021 at 06:49):

Where from?

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

from here

Yves Bertot (Jun 01 2021 at 06:57):

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: Nov 29 2023 at 18:01 UTC