Strict inequality of real numbers
Content created by Louis Wasserman, Fredrik Bakke, Egbert Rijke and Vojtěch Štěpančík.
Created on 2025-02-05.
Last modified on 2025-09-06.
{-# OPTIONS --lossy-unification #-} module real-numbers.strict-inequality-real-numbers where
Imports
open import elementary-number-theory.addition-rational-numbers open import elementary-number-theory.additive-group-of-rational-numbers open import elementary-number-theory.difference-rational-numbers open import elementary-number-theory.positive-rational-numbers open import elementary-number-theory.rational-numbers open import elementary-number-theory.strict-inequality-rational-numbers open import foundation.action-on-identifications-functions open import foundation.binary-transport open import foundation.cartesian-product-types open import foundation.conjunction open import foundation.coproduct-types open import foundation.dependent-pair-types open import foundation.disjunction open import foundation.empty-types open import foundation.existential-quantification open import foundation.function-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-disjunction open import foundation.identity-types open import foundation.large-binary-relations open import foundation.logical-equivalences open import foundation.negation open import foundation.propositional-truncations open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.transport-along-identifications open import foundation.type-arithmetic-cartesian-product-types open import foundation.universe-levels open import group-theory.abelian-groups open import logic.functoriality-existential-quantification open import real-numbers.addition-real-numbers open import real-numbers.arithmetically-located-dedekind-cuts open import real-numbers.dedekind-real-numbers open import real-numbers.difference-real-numbers open import real-numbers.inequality-real-numbers open import real-numbers.negation-real-numbers open import real-numbers.rational-real-numbers open import real-numbers.similarity-real-numbers
Idea
The standard strict ordering¶ on the real numbers is defined as the presence of a rational number between them. This is the definition used in [UF13], section 11.2.1.
opaque le-ℝ : Large-Relation _⊔_ ℝ le-ℝ x y = exists ℚ (λ q → upper-cut-ℝ x q ∧ lower-cut-ℝ y q) is-prop-le-ℝ : {l1 l2 : Level} → (x : ℝ l1) (y : ℝ l2) → is-prop (le-ℝ x y) is-prop-le-ℝ x y = is-prop-exists ℚ (λ q → upper-cut-ℝ x q ∧ lower-cut-ℝ y q) le-prop-ℝ : Large-Relation-Prop _⊔_ ℝ le-prop-ℝ x y = (le-ℝ x y , is-prop-le-ℝ x y)
Properties
Strict inequality on the reals implies inequality
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ leq-ℝ leq-le-ℝ : le-ℝ x y → leq-ℝ x y leq-le-ℝ x<y p p<x = elim-exists ( lower-cut-ℝ y p) ( λ q (x<q , q<y) → le-lower-cut-ℝ y p q (le-lower-upper-cut-ℝ x p q p<x x<q) q<y) ( x<y)
Strict inequality on the reals is irreflexive
module _ {l : Level} (x : ℝ l) where opaque unfolding le-ℝ irreflexive-le-ℝ : ¬ (le-ℝ x x) irreflexive-le-ℝ = elim-exists ( empty-Prop) ( λ q (x<q , q<x) → is-disjoint-cut-ℝ x q (q<x , x<q))
Strict inequality on the reals is asymmetric
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ asymmetric-le-ℝ : le-ℝ x y → ¬ (le-ℝ y x) asymmetric-le-ℝ x<y y<x = let open do-syntax-trunc-Prop empty-Prop in do ( p , x<p , p<y) ← x<y ( q , y<q , q<x) ← y<x rec-coproduct ( asymmetric-le-ℚ ( q) ( p) ( le-lower-upper-cut-ℝ x q p q<x x<p)) ( not-leq-le-ℚ ( p) ( q) ( le-lower-upper-cut-ℝ y p q p<y y<q)) ( decide-le-leq-ℚ p q)
Strict inequality on the reals is transitive
module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where opaque unfolding le-ℝ transitive-le-ℝ : le-ℝ y z → le-ℝ x y → le-ℝ x z transitive-le-ℝ y<z x<y = let open do-syntax-trunc-Prop (le-prop-ℝ x z) in do ( p , x<p , p<y) ← x<y ( q , y<q , q<z) ← y<z intro-exists ( p) ( x<p , le-lower-cut-ℝ z p q (le-lower-upper-cut-ℝ y p q p<y y<q) q<z)
The canonical map from rationals to reals preserves and reflects strict inequality
module _ (x y : ℚ) where opaque unfolding le-ℝ real-ℚ preserves-le-real-ℚ : le-ℚ x y → le-ℝ (real-ℚ x) (real-ℚ y) preserves-le-real-ℚ x<y = intro-exists ( mediant-ℚ x y) ( le-left-mediant-ℚ x y x<y , le-right-mediant-ℚ x y x<y) reflects-le-real-ℚ : le-ℝ (real-ℚ x) (real-ℚ y) → le-ℚ x y reflects-le-real-ℚ = elim-exists ( le-ℚ-Prop x y) ( λ q (x<q , q<y) → transitive-le-ℚ x q y q<y x<q) iff-le-real-ℚ : le-ℚ x y ↔ le-ℝ (real-ℚ x) (real-ℚ y) pr1 iff-le-real-ℚ = preserves-le-real-ℚ pr2 iff-le-real-ℚ = reflects-le-real-ℚ
Concatenation rules for inequality and strict inequality on the real numbers
module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where opaque unfolding le-ℝ leq-ℝ leq-ℝ' concatenate-le-leq-ℝ : le-ℝ x y → leq-ℝ y z → le-ℝ x z concatenate-le-leq-ℝ x<y y≤z = map-tot-exists (λ p → map-product id (y≤z p)) x<y concatenate-leq-le-ℝ : leq-ℝ x y → le-ℝ y z → le-ℝ x z concatenate-leq-le-ℝ x≤y = map-tot-exists ( λ p → map-product (forward-implication (leq-iff-ℝ' x y) x≤y p) id)
A rational is in the lower cut of x
iff its real projection is less than x
module _ {l : Level} (q : ℚ) (x : ℝ l) where opaque unfolding le-ℝ real-ℚ le-real-iff-lower-cut-ℚ : is-in-lower-cut-ℝ x q ↔ le-ℝ (real-ℚ q) x le-real-iff-lower-cut-ℚ = is-rounded-lower-cut-ℝ x q abstract le-real-is-in-lower-cut-ℚ : is-in-lower-cut-ℝ x q → le-ℝ (real-ℚ q) x le-real-is-in-lower-cut-ℚ = forward-implication le-real-iff-lower-cut-ℚ is-in-lower-cut-le-real-ℚ : le-ℝ (real-ℚ q) x → is-in-lower-cut-ℝ x q is-in-lower-cut-le-real-ℚ = backward-implication le-real-iff-lower-cut-ℚ
A rational is in the upper cut of x
iff its real projection is greater than x
module _ {l : Level} (q : ℚ) (x : ℝ l) where opaque unfolding le-ℝ real-ℚ le-iff-upper-cut-real-ℚ : is-in-upper-cut-ℝ x q ↔ le-ℝ x (real-ℚ q) le-iff-upper-cut-real-ℚ = iff-tot-exists (λ _ → iff-equiv commutative-product) ∘iff is-rounded-upper-cut-ℝ x q abstract le-real-is-in-upper-cut-ℚ : is-in-upper-cut-ℝ x q → le-ℝ x (real-ℚ q) le-real-is-in-upper-cut-ℚ = forward-implication le-iff-upper-cut-real-ℚ is-in-upper-cut-le-real-ℚ : le-ℝ x (real-ℚ q) → is-in-upper-cut-ℝ x q is-in-upper-cut-le-real-ℚ = backward-implication le-iff-upper-cut-real-ℚ
The real numbers are located
module _ {l : Level} (x : ℝ l) (p q : ℚ) (p<q : le-ℚ p q) where is-located-le-ℝ : disjunction-type (le-ℝ (real-ℚ p) x) (le-ℝ x (real-ℚ q)) is-located-le-ℝ = map-disjunction ( le-real-is-in-lower-cut-ℚ p x) ( le-real-is-in-upper-cut-ℚ q x) ( is-located-lower-upper-cut-ℝ x p q p<q)
Every real is less than a rational number
module _ {l : Level} (x : ℝ l) where abstract le-some-rational-ℝ : exists ℚ (λ q → le-prop-ℝ x (real-ℚ q)) le-some-rational-ℝ = map-tot-exists ( λ q → le-real-is-in-upper-cut-ℚ q x) ( is-inhabited-upper-cut-ℝ x)
The reals have no lower or upper bound
module _ {l : Level} (x : ℝ l) where abstract exists-lesser-ℝ : exists (ℝ lzero) (λ y → le-prop-ℝ y x) exists-lesser-ℝ = let open do-syntax-trunc-Prop (∃ (ℝ lzero) (λ y → le-prop-ℝ y x)) in do ( q , q<x) ← is-inhabited-lower-cut-ℝ x intro-exists (real-ℚ q) (le-real-is-in-lower-cut-ℚ q x q<x) exists-greater-ℝ : exists (ℝ lzero) (λ y → le-prop-ℝ x y) exists-greater-ℝ = let open do-syntax-trunc-Prop (∃ (ℝ lzero) (le-prop-ℝ x)) in do ( q , x<q) ← is-inhabited-upper-cut-ℝ x intro-exists (real-ℚ q) (le-real-is-in-upper-cut-ℚ q x x<q)
Negation reverses the strict ordering of real numbers
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ neg-ℝ neg-le-ℝ : le-ℝ x y → le-ℝ (neg-ℝ y) (neg-ℝ x) neg-le-ℝ x<y = let open do-syntax-trunc-Prop (le-prop-ℝ (neg-ℝ y) (neg-ℝ x)) in do (p , x<p , p<y) ← x<y intro-exists ( neg-ℚ p) ( inv-tr (is-in-lower-cut-ℝ y) (neg-neg-ℚ p) p<y , inv-tr (is-in-upper-cut-ℝ x) (neg-neg-ℚ p) x<p)
If x
is less than y
, then y
is not less than or equal to x
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ leq-ℝ not-leq-le-ℝ : le-ℝ x y → ¬ (leq-ℝ y x) not-leq-le-ℝ x<y y≤x = elim-exists ( empty-Prop) ( λ q (x<q , q<y) → is-disjoint-cut-ℝ x q (y≤x q q<y , x<q)) ( x<y)
If x
is not less than y
, then y
is less than or equal to x
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ leq-ℝ leq-not-le-ℝ : ¬ (le-ℝ x y) → leq-ℝ y x leq-not-le-ℝ x≮y p p<y = let open do-syntax-trunc-Prop (lower-cut-ℝ x p) in do ( q , p<q , q<y) ← forward-implication (is-rounded-lower-cut-ℝ y p) p<y elim-disjunction ( lower-cut-ℝ x p) ( id) ( λ x<q → reductio-ad-absurdum (intro-exists q (x<q , q<y)) x≮y) ( is-located-lower-upper-cut-ℝ x p q p<q)
If x
is less than or equal to y
, then y
is not less than x
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where not-le-leq-ℝ : leq-ℝ x y → ¬ (le-ℝ y x) not-le-leq-ℝ x≤y y<x = not-leq-le-ℝ y x y<x x≤y
x
is less than or equal to y
if and only if y
is not less than x
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where leq-iff-not-le-ℝ : leq-ℝ x y ↔ ¬ (le-ℝ y x) pr1 leq-iff-not-le-ℝ = not-le-leq-ℝ x y pr2 leq-iff-not-le-ℝ = leq-not-le-ℝ y x
The rational numbers are dense in the real numbers
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding le-ℝ real-ℚ dense-rational-le-ℝ : le-ℝ x y → exists ℚ (λ z → le-prop-ℝ x (real-ℚ z) ∧ le-prop-ℝ (real-ℚ z) y) dense-rational-le-ℝ x<y = let open do-syntax-trunc-Prop ( ∃ ℚ (λ z → le-prop-ℝ x (real-ℚ z) ∧ le-prop-ℝ (real-ℚ z) y)) in do ( q , x<q , q<y) ← x<y ( p , p<q , x<p) ← forward-implication (is-rounded-upper-cut-ℝ x q) x<q ( r , q<r , r<y) ← forward-implication (is-rounded-lower-cut-ℝ y q) q<y intro-exists ( q) ( intro-exists p (x<p , p<q) , intro-exists r (q<r , r<y))
Strict inequality on the real numbers is dense
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where abstract dense-le-ℝ : le-ℝ x y → exists (ℝ lzero) (λ z → le-prop-ℝ x z ∧ le-prop-ℝ z y) dense-le-ℝ x<y = map-exists ( _) ( real-ℚ) ( λ _ → id) ( dense-rational-le-ℝ x y x<y)
Strict inequality on the real numbers is cotransitive
opaque unfolding le-ℝ cotransitive-le-ℝ : is-cotransitive-Large-Relation-Prop ℝ le-prop-ℝ cotransitive-le-ℝ x y z x<y = let open do-syntax-trunc-Prop (le-prop-ℝ x z ∨ le-prop-ℝ z y) in do ( q , x<q , q<y) ← x<y ( p , p<q , x<p) ← forward-implication (is-rounded-upper-cut-ℝ x q) x<q map-disjunction ( λ p<z → intro-exists p (x<p , p<z)) ( λ z<q → intro-exists q (z<q , q<y)) ( is-located-lower-upper-cut-ℝ z p q p<q)
Strict inequality on the real numbers is invariant under similarity
module _ {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) (x~y : sim-ℝ x y) where opaque unfolding le-ℝ sim-ℝ preserves-le-left-sim-ℝ : le-ℝ x z → le-ℝ y z preserves-le-left-sim-ℝ = map-tot-exists ( λ q → map-product ( pr1 (sim-upper-cut-sim-ℝ x y x~y) q) ( id)) preserves-le-right-sim-ℝ : le-ℝ z x → le-ℝ z y preserves-le-right-sim-ℝ = map-tot-exists ( λ q → map-product id (pr1 x~y q)) module _ {l1 l2 l3 l4 : Level} (x1 : ℝ l1) (x2 : ℝ l2) (y1 : ℝ l3) (y2 : ℝ l4) (x1~x2 : sim-ℝ x1 x2) (y1~y2 : sim-ℝ y1 y2) where preserves-le-sim-ℝ : le-ℝ x1 y1 → le-ℝ x2 y2 preserves-le-sim-ℝ x1<y1 = preserves-le-left-sim-ℝ ( y2) ( x1) ( x2) ( x1~x2) ( preserves-le-right-sim-ℝ x1 y1 y2 y1~y2 x1<y1)
Strict inequality on the real numbers is translation invariant
module _ {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) where opaque unfolding add-ℝ le-ℝ preserves-le-right-add-ℝ : le-ℝ x y → le-ℝ (x +ℝ z) (y +ℝ z) preserves-le-right-add-ℝ x<y = let open do-syntax-trunc-Prop ( ∃ ℚ (λ r → upper-cut-ℝ (x +ℝ z) r ∧ lower-cut-ℝ (y +ℝ z) r)) in do ( p , x<p , p<y) ← x<y ( q , p<q , q<y) ← forward-implication (is-rounded-lower-cut-ℝ y p) p<y ( (r , s) , s<r+q-p , r<z , z<s) ← is-arithmetically-located-ℝ ( z) ( positive-diff-le-ℚ p q p<q) let p-q+s<r : le-ℚ ((p -ℚ q) +ℚ s) r p-q+s<r = tr ( le-ℚ ((p -ℚ q) +ℚ s)) ( equational-reasoning (p -ℚ q) +ℚ (r +ℚ (q -ℚ p)) = (p -ℚ q) +ℚ (r -ℚ (p -ℚ q)) by ap ( λ t → (p -ℚ q) +ℚ (r +ℚ t)) ( inv (distributive-neg-diff-ℚ p q)) = r by is-identity-right-conjugation-add-ℚ (p -ℚ q) r) ( preserves-le-right-add-ℚ (p -ℚ q) s (r +ℚ (q -ℚ p)) s<r+q-p) intro-exists ( p +ℚ s) ( intro-exists (p , s) (x<p , z<s , refl) , intro-exists ( q , (p -ℚ q) +ℚ s) ( q<y , le-lower-cut-ℝ z ((p -ℚ q) +ℚ s) r p-q+s<r r<z , ( equational-reasoning p +ℚ s = (q +ℚ (p -ℚ q)) +ℚ s by ap ( _+ℚ s) ( inv (is-identity-right-conjugation-add-ℚ q p)) = q +ℚ ((p -ℚ q) +ℚ s) by associative-add-ℚ _ _ _))) preserves-le-left-add-ℝ : le-ℝ x y → le-ℝ (z +ℝ x) (z +ℝ y) preserves-le-left-add-ℝ x<y = binary-tr ( le-ℝ) ( commutative-add-ℝ x z) ( commutative-add-ℝ y z) ( preserves-le-right-add-ℝ x<y) abstract preserves-le-diff-ℝ : {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) → le-ℝ x y → le-ℝ (x -ℝ z) (y -ℝ z) preserves-le-diff-ℝ z = preserves-le-right-add-ℝ (neg-ℝ z) reverses-le-diff-ℝ : {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) → le-ℝ x y → le-ℝ (z -ℝ y) (z -ℝ x) reverses-le-diff-ℝ z x y x<y = preserves-le-left-add-ℝ z _ _ (neg-le-ℝ _ _ x<y) module _ {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) where abstract reflects-le-right-add-ℝ : le-ℝ (x +ℝ z) (y +ℝ z) → le-ℝ x y reflects-le-right-add-ℝ x+z<y+z = preserves-le-sim-ℝ ( (x +ℝ z) +ℝ neg-ℝ z) ( x) ( (y +ℝ z) +ℝ neg-ℝ z) ( y) ( cancel-right-add-diff-ℝ x z) ( cancel-right-add-diff-ℝ y z) ( preserves-le-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z<y+z) reflects-le-left-add-ℝ : le-ℝ (z +ℝ x) (z +ℝ y) → le-ℝ x y reflects-le-left-add-ℝ z+x<z+y = reflects-le-right-add-ℝ ( binary-tr ( le-ℝ) ( commutative-add-ℝ z x) ( commutative-add-ℝ z y) ( z+x<z+y)) module _ {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) where iff-translate-right-le-ℝ : le-ℝ x y ↔ le-ℝ (x +ℝ z) (y +ℝ z) pr1 iff-translate-right-le-ℝ = preserves-le-right-add-ℝ z x y pr2 iff-translate-right-le-ℝ = reflects-le-right-add-ℝ z x y iff-translate-left-le-ℝ : le-ℝ x y ↔ le-ℝ (z +ℝ x) (z +ℝ y) pr1 iff-translate-left-le-ℝ = preserves-le-left-add-ℝ z x y pr2 iff-translate-left-le-ℝ = reflects-le-left-add-ℝ z x y abstract preserves-le-add-ℝ : {l1 l2 l3 l4 : Level} (a : ℝ l1) (b : ℝ l2) (c : ℝ l3) (d : ℝ l4) → le-ℝ a b → le-ℝ c d → le-ℝ (a +ℝ c) (b +ℝ d) preserves-le-add-ℝ a b c d a≤b c≤d = transitive-le-ℝ ( a +ℝ c) ( a +ℝ d) ( b +ℝ d) ( preserves-le-right-add-ℝ d a b a≤b) ( preserves-le-left-add-ℝ a c d c≤d)
x + y < z
if and only if x < z - y
module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract le-transpose-left-add-ℝ : le-ℝ (x +ℝ y) z → le-ℝ x (z -ℝ y) le-transpose-left-add-ℝ x+y<z = preserves-le-left-sim-ℝ ( z -ℝ y) ( (x +ℝ y) -ℝ y) ( x) ( cancel-right-add-diff-ℝ x y) ( preserves-le-right-add-ℝ (neg-ℝ y) (x +ℝ y) z x+y<z) module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract le-transpose-left-add-ℝ' : le-ℝ (x +ℝ y) z → le-ℝ y (z -ℝ x) le-transpose-left-add-ℝ' x+y<z = le-transpose-left-add-ℝ y x z ( tr (λ w → le-ℝ w z) (commutative-add-ℝ _ _) x+y<z) module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract le-transpose-right-diff-ℝ : le-ℝ x (y -ℝ z) → le-ℝ (x +ℝ z) y le-transpose-right-diff-ℝ x<y-z = preserves-le-right-sim-ℝ ( x +ℝ z) ( (y -ℝ z) +ℝ z) ( y) ( cancel-right-diff-add-ℝ y z) ( preserves-le-right-add-ℝ z x (y -ℝ z) x<y-z) le-transpose-right-diff-ℝ' : le-ℝ x (y -ℝ z) → le-ℝ (z +ℝ x) y le-transpose-right-diff-ℝ' x<y-z = tr ( λ w → le-ℝ w y) ( commutative-add-ℝ _ _) ( le-transpose-right-diff-ℝ x<y-z) module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where iff-diff-right-le-ℝ : le-ℝ (x +ℝ y) z ↔ le-ℝ x (z -ℝ y) iff-diff-right-le-ℝ = (le-transpose-left-add-ℝ x y z , le-transpose-right-diff-ℝ x z y) module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract iff-add-right-le-ℝ : le-ℝ (x -ℝ y) z ↔ le-ℝ x (z +ℝ y) iff-add-right-le-ℝ = tr ( λ w → le-ℝ (x -ℝ y) z ↔ le-ℝ x (z +ℝ w)) ( neg-neg-ℝ y) ( iff-diff-right-le-ℝ x (neg-ℝ y) z) le-transpose-left-diff-ℝ : le-ℝ (x -ℝ y) z → le-ℝ x (z +ℝ y) le-transpose-left-diff-ℝ = forward-implication iff-add-right-le-ℝ module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract le-transpose-right-add-ℝ : le-ℝ x (y +ℝ z) → le-ℝ (x -ℝ z) y le-transpose-right-add-ℝ = backward-implication (iff-add-right-le-ℝ x z y) module _ {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) where abstract le-transpose-right-add-ℝ' : le-ℝ x (y +ℝ z) → le-ℝ (x -ℝ y) z le-transpose-right-add-ℝ' x<y+z = le-transpose-right-add-ℝ x z y (tr (le-ℝ x) (commutative-add-ℝ _ _) x<y+z)
If x < y
, then there is some ε : ℚ⁺
with x + ε < y
module _ {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} (x<y : le-ℝ x y) where abstract exists-positive-rational-separation-le-ℝ : exists ℚ⁺ (λ q → le-prop-ℝ (x +ℝ real-ℚ⁺ q) y) exists-positive-rational-separation-le-ℝ = let open do-syntax-trunc-Prop (∃ ℚ⁺ (λ q → le-prop-ℝ (x +ℝ real-ℚ⁺ q) y)) in do (q , 0<q , q<y-x) ← dense-rational-le-ℝ zero-ℝ (y -ℝ x) ( preserves-le-left-sim-ℝ ( y -ℝ x) ( x -ℝ x) ( zero-ℝ) ( right-inverse-law-add-ℝ x) ( preserves-le-right-add-ℝ (neg-ℝ x) x y x<y)) intro-exists ( q , is-positive-le-zero-ℚ q (reflects-le-real-ℚ _ _ 0<q)) ( le-transpose-right-diff-ℝ' _ _ _ q<y-x)
If x < y + ε
for every positive rational ε
, then x ≤ y
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where abstract saturated-le-ℝ : ((ε : ℚ⁺) → le-ℝ x (y +ℝ real-ℚ⁺ ε)) → leq-ℝ x y saturated-le-ℝ H = leq-not-le-ℝ y x ( λ y<x → let open do-syntax-trunc-Prop empty-Prop in do (ε , y+ε<x) ← exists-positive-rational-separation-le-ℝ {x = y} {y = x} y<x irreflexive-le-ℝ ( x) ( transitive-le-ℝ x (y +ℝ real-ℚ⁺ ε) x y+ε<x (H ε)))
If x
is less than each rational number y
is less than, then x ≤ y
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where opaque unfolding leq-ℝ' leq-le-rational-ℝ : ((q : ℚ) → le-ℝ y (real-ℚ q) → le-ℝ x (real-ℚ q)) → leq-ℝ x y leq-le-rational-ℝ H = leq-leq'-ℝ _ _ ( λ q y<q → is-in-upper-cut-le-real-ℚ q x ( H q (le-real-is-in-upper-cut-ℚ q y y<q)))
Two real numbers are similar if they are less than the same rational numbers
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) where abstract sim-le-same-rational-ℝ : ((q : ℚ) → le-ℝ x (real-ℚ q) ↔ le-ℝ y (real-ℚ q)) → sim-ℝ x y sim-le-same-rational-ℝ H = sim-sim-leq-ℝ ( leq-le-rational-ℝ x y (backward-implication ∘ H) , leq-le-rational-ℝ y x (forward-implication ∘ H))
If x + y < p
for some rational p
, then there exist q r : ℚ
such that p = q + r
, x < q
, y < r
module _ {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) (p : ℚ) where opaque unfolding add-ℝ le-split-add-rational-ℝ : le-ℝ (x +ℝ y) (real-ℚ p) → exists ( ℚ × ℚ) ( λ (q , r) → Id-Prop ℚ-Set p (q +ℚ r) ∧ le-prop-ℝ x (real-ℚ q) ∧ le-prop-ℝ y (real-ℚ r)) le-split-add-rational-ℝ x+y<p = let open do-syntax-trunc-Prop (∃ _ _) in do ((q , r) , x<q , y<r , p=q+r) ← is-in-upper-cut-le-real-ℚ p (x +ℝ y) x+y<p intro-exists ( q , r) ( p=q+r , le-real-is-in-upper-cut-ℚ q x x<q , le-real-is-in-upper-cut-ℚ r y y<r)
References
- [UF13]
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.
Recent changes
- 2025-09-06. Louis Wasserman. Metrics of metric spaces (#1532).
- 2025-09-02. Louis Wasserman. Maximum and minimum of finite families of real numbers (#1522).
- 2025-09-02. Louis Wasserman. Metric spaces induced by metric functions (#1520).
- 2025-09-02. Louis Wasserman. Opacify real numbers (#1521).
- 2025-08-30. Louis Wasserman. Suprema and infima of families of real numbers (#1504).