From 3a32dae43ef87b02ea82629b757acae8fbea98f4 Mon Sep 17 00:00:00 2001 From: malarbol Date: Tue, 27 Feb 2024 19:04:57 +0100 Subject: [PATCH] Update src/real-numbers/rational-real-numbers.lagda.md Co-authored-by: Fredrik Bakke --- src/real-numbers/rational-real-numbers.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md index 2ef3432f82..878b9e33fc 100644 --- a/src/real-numbers/rational-real-numbers.lagda.md +++ b/src/real-numbers/rational-real-numbers.lagda.md @@ -211,8 +211,8 @@ eq-real-rational-is-rational-ℝ x q H = ( is-located-lower-upper-cut-ℝ x r q I)) ( trichotomy-le-ℚ r q ( λ I _ → I) - ( λ E H' → ex-falso ( pr1 ( tr ( is-rational-ℝ x) ( inv E) H) H')) - ( λ I H' → ex-falso ( pr1 H ( le-lower-cut-ℝ x q r I H')))))) + ( λ E H' → ex-falso (pr1 (tr (is-rational-ℝ x) (inv E) H) H')) + ( λ I H' → ex-falso (pr1 H (le-lower-cut-ℝ x q r I H')))))) ``` ### The cannonical map from rationals to rational reals