Apartness for real numbers #1296
Conversation
|
Forgot this depended on #1288. |
|
Reopening now that the dependency is merged. |
| nonequal-apart-ℝ : apart-ℝ x y → x ≠ y | ||
| nonequal-apart-ℝ apart x=y = | ||
| elim-disjunction | ||
| ( empty-Prop) | ||
| ( λ x<y → irreflexive-le-ℝ x (tr (le-ℝ x) (inv x=y) x<y)) | ||
| ( λ y<x → irreflexive-le-ℝ y (tr (le-ℝ y) x=y y<x)) | ||
| ( apart) |
There was a problem hiding this comment.
This is a general result about apartness relations and should be added to foundation.apartness-relations, which this file should depend on.
There was a problem hiding this comment.
I'm assuming this implies I need to add large apartness relations.
There was a problem hiding this comment.
That would be great :)))
I have some additions I wrote for apartness relations in an unmerged branch. It might be helpful to start from that. It's in the logic-compactness branch. I'll find a link later.
| ( apart) | ||
| ``` | ||
|
|
||
| ### If LEM, inequality implies apartness |
There was a problem hiding this comment.
Inequality is a different concept from negated equality/nonequality.
| ### If LEM, inequality implies apartness | |
| ### Assuming the law of excluded middle, nonequal real numbers are apart |
|
I'm marking this PR as a draft until the work has been integrated with our infrastructure for apartness relations |
|
I hadn't noticed that was a thing. Oops. Let me do that. |
Apartness from 0, for example, implies a real is multiplicatively invertible.