Yves Bertot (May 31 2021 at 09:29): 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?
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.
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.
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.
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