coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about proving the domain of a real-valued function

From: <ncyms8r3x2 AT snkmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about proving the domain of a real-valued function
Date: Wed, 12 Nov 2014 08:03:19 +0100

Let's say I have a function:
Definition f (x:R) := (x + 1)/(x - 1).

Is there anyway to prove what that 1 isn't in its domain?

Are there any good tutorials on using the Reals module from the standard
library?

[Coq-Club] Question about proving the domain of a real-valued function, ncyms8r3x2, 11/12/2014
- Re: [Coq-Club] Question about proving the domain of a real-valued function, Guillaume Melquiond, 11/12/2014