The difference between real numbers

Content created by Louis Wasserman.

Created on 2025-03-27.
Last modified on 2025-04-25.

{-# OPTIONS --lossy-unification #-}

module real-numbers.difference-real-numbers where
Imports
open import elementary-number-theory.difference-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import real-numbers.addition-real-numbers
open import real-numbers.dedekind-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 difference of two real numbers x and y is the sum of x and the negation of y.

Definition

diff-ℝ : {l1 l2 : Level}  (x :  l1)  (y :  l2)   (l1  l2)
diff-ℝ x y = add-ℝ x (neg-ℝ y)

infixl 36 _-ℝ_
_-ℝ_ = diff-ℝ

Properties

The inclusion of rational numbers preserves differences

abstract
  diff-real-ℚ : (p q : )  (real-ℚ p) -ℝ (real-ℚ q)  real-ℚ (p -ℚ q)
  diff-real-ℚ p q = ap (real-ℚ p +ℝ_) (neg-real-ℚ q)  add-real-ℚ p (neg-ℚ q)

The negative of the difference of x and y is the difference of y and x

module _
  {l1 l2 : Level} (x :  l1) (y :  l2)
  where

  abstract
    distributive-neg-diff-ℝ : neg-ℝ (x -ℝ y)  y -ℝ x
    distributive-neg-diff-ℝ =
      equational-reasoning
        neg-ℝ (x -ℝ y)
         neg-ℝ x +ℝ neg-ℝ (neg-ℝ y) by distributive-neg-add-ℝ _ _
         neg-ℝ x +ℝ y by ap (neg-ℝ x +ℝ_) (neg-neg-ℝ y)
         y -ℝ x by commutative-add-ℝ _ _

Interchange laws for addition and difference on real numbers

module _
  {l1 l2 l3 l4 : Level} (a :  l1) (b :  l2) (c :  l3) (d :  l4)
  where

  abstract
    interchange-law-diff-add-ℝ :
      (a +ℝ b) -ℝ (c +ℝ d)  (a -ℝ c) +ℝ (b -ℝ d)
    interchange-law-diff-add-ℝ =
      ( ap ((a +ℝ b) +ℝ_) (distributive-neg-add-ℝ c d)) 
      ( interchange-law-add-add-ℝ _ _ _ _)

Recent changes