Stream: math-comp analysis

Topic: Getting started with mathcomp-analysis : continuo...


view this post on Zulip Yves Bertot (May 31 2021 at 09:29):

Hello, how can I write the statement "sqrtr is continuous" in an environment where reals, topology, normedtype, landau, and derive from mathcomp.analysis have been loaded?

view this post on Zulip Yves Bertot (May 31 2021 at 10:47):

I tried writing the following:

Lemma sqrt_continuous :  continuous (@Num.sqrt R).```

but I get a phantom error message which seems to indicate that my type is not located correctly in the hierarchy.

view this post on Zulip Reynald Affeldt (May 31 2021 at 11:25):

Would this be good enough?

From mathcomp Require Import all_ssreflect ssralg ssrnum.
Require Import boolp reals classical_sets topology.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import numFieldTopology.Exports.

Lemma sqrt_continuous (R : realType) : continuous (@Num.sqrt R).
Abort.

Require Import Reals Rstruct.

Lemma sqrt_continuous : continuous (@Num.sqrt [rcfType of R]).
Abort.

view this post on Zulip Yves Bertot (May 31 2021 at 11:43):

Thanks, the difficulty for me was that Require Import ... topology is not enough, I also need the line you included:

Import numFieldTopology.Exports.

I will keep experimenting.

view this post on Zulip Notification Bot (Jun 01 2021 at 10:09):

This topic was moved here from #math-comp users > Getting started with mathcomp-analysis : continuo... by Cyril Cohen


Last updated: Aug 11 2022 at 01:03 UTC