Stream: math-comp analysis

Topic: Using natmul_continuous on the support realType


view this post on Zulip 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.

view this post on Zulip Yves Bertot (Jun 01 2021 at 06:28):

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

view this post on Zulip Laurent Théry (Jun 01 2021 at 06:40):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Laurent Théry (Jun 01 2021 at 06:48):

I just copy and paste headers :flushed:

view this post on Zulip Yves Bertot (Jun 01 2021 at 06:49):

Where from?

view this post on Zulip Laurent Théry (Jun 01 2021 at 06:53):

from here

view this post on Zulip Yves Bertot (Jun 01 2021 at 06:57):

Thanks

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC