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.
I should have said that
R : realType in this context.
You must have the wrong import. Your example works in my setting.
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
Thansk, this solves my problem in the short term. How do you make sure to have the right sequence of imports?
I just copy and paste headers :flushed:
This topic was moved here from #math-comp users > Using natmul_continuous on the support realType by Cyril Cohen
Last updated: Feb 05 2023 at 07:03 UTC