Theory hreal

⊢ ∀x. cut_of_hrat x = (λy. y hrat_lt x)

⊢ ∀x y. x hrat_lt y ⇔ ∃d. y = x hrat_add d

⊢ hreal_1 = hreal (cut_of_hrat hrat_1)

⊢ ∃rep. TYPE_DEFINITION isacut rep

⊢ ∀X Y.
    X hreal_add Y =
    hreal (λw. ∃x y. (w = x hrat_add y) ∧ cut X x ∧ cut Y y)

⊢ ∀X. hreal_inv X =
      hreal
        (λw. ∃d. d hrat_lt hrat_1 ∧ ∀x. cut X x ⇒ w hrat_mul x hrat_lt d)

⊢ ∀X Y. X hreal_lt Y ⇔ X ≠ Y ∧ ∀x. cut X x ⇒ cut Y x

⊢ ∀X Y.
    X hreal_mul Y =
    hreal (λw. ∃x y. (w = x hrat_mul y) ∧ cut X x ∧ cut Y y)

⊢ ∀x y. hreal_of_treal (x,y) = @d. x = y hreal_add d

⊢ ∀Y X. Y hreal_sub X = hreal (λw. ∃x. ¬cut X x ∧ cut Y (x hrat_add w))

⊢ ∀P. hreal_sup P = hreal (λw. ∃X. P X ∧ cut X w)

⊢ (∀a. hreal (cut a) = a) ∧ ∀r. isacut r ⇔ (cut (hreal r) = r)

⊢ ∀C. isacut C ⇔
      (∃x. C x) ∧ (∃x. ¬C x) ∧ (∀x y. C x ∧ y hrat_lt x ⇒ C y) ∧
      ∀x. C x ⇒ ∃y. C y ∧ x hrat_lt y

⊢ treal_0 = (hreal_1,hreal_1)

⊢ treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)

⊢ ∀x1 y1 x2 y2.
    (x1,y1) treal_add (x2,y2) = (x1 hreal_add x2,y1 hreal_add y2)

⊢ ∀x1 y1 x2 y2.
    (x1,y1) treal_eq (x2,y2) ⇔ (x1 hreal_add y2 = x2 hreal_add y1)

⊢ ∀x y.
    treal_inv (x,y) =
    if x = y then treal_0
    else if y hreal_lt x then
      (hreal_inv (x hreal_sub y) hreal_add hreal_1,hreal_1)
    else (hreal_1,hreal_inv (y hreal_sub x) hreal_add hreal_1)

⊢ ∀x1 y1 x2 y2.
    (x1,y1) treal_lt (x2,y2) ⇔ x1 hreal_add y2 hreal_lt x2 hreal_add y1

⊢ ∀x1 y1 x2 y2.
    (x1,y1) treal_mul (x2,y2) =
    (x1 hreal_mul x2 hreal_add y1 hreal_mul y2,
     x1 hreal_mul y2 hreal_add y1 hreal_mul x2)

⊢ ∀x y. treal_neg (x,y) = (y,x)

⊢ ∀x. treal_of_hreal x = (x hreal_add hreal_1,hreal_1)

⊢ ∀X. ∃x. ¬cut X x

⊢ ∀X x y. cut X x ∧ y hrat_lt x ⇒ cut X y

⊢ ∀X. isacut (cut X)

⊢ ∀X e. ∃x. cut X x ∧ ¬cut X (x hrat_add e)

⊢ ∀X u. hrat_1 hrat_lt u ⇒ ∃x. cut X x ∧ ¬cut X (u hrat_mul x)

⊢ ∀X. ∃x. cut X x

⊢ ∀X x y. cut X x ∧ ¬cut X y ⇒ x hrat_lt y

⊢ ∀X x y. ¬cut X x ∧ x hrat_lt y ⇒ ¬cut X y

⊢ ∀X x. cut X x ⇒ ∃y. cut X y ∧ x hrat_lt y

⊢ ∀X Y. (cut X = cut Y) ⇒ (X = Y)

⊢ ∀x. ∃y. y hrat_lt x

⊢ ∀x y. ∃z. z hrat_lt x ∧ z hrat_lt y

⊢ ∀x y z. (x hrat_add y = x hrat_add z) ⇔ (y = z)

⊢ ∀x y z. (x hrat_mul y = x hrat_mul z) ⇔ (y = z)

⊢ ∀x y. hrat_1 hrat_lt hrat_inv x hrat_mul y ⇔ x hrat_lt y

⊢ ∀x y. y hrat_lt x hrat_mul y ⇔ hrat_1 hrat_lt x

⊢ ∀x y. hrat_inv (x hrat_mul y) = hrat_inv x hrat_mul hrat_inv y

⊢ ∀u v x y. u hrat_lt x ∧ v hrat_lt y ⇒ u hrat_add v hrat_lt x hrat_add y

⊢ ∀x y. x hrat_lt x hrat_add y

⊢ ∀x y. y hrat_lt x hrat_add y

⊢ ∀x y. ¬(x hrat_lt y ∧ y hrat_lt x)

⊢ ∀x y. x hrat_lt y ⇒ ¬(y hrat_lt x)

⊢ ∀x y. hrat_inv x hrat_mul y hrat_lt hrat_1 ⇔ y hrat_lt x

⊢ ∀x y z. z hrat_add x hrat_lt z hrat_add y ⇔ x hrat_lt y

⊢ ∀x y z. z hrat_mul x hrat_lt z hrat_mul y ⇔ x hrat_lt y

⊢ ∀x y. x hrat_mul y hrat_lt y ⇔ x hrat_lt hrat_1

⊢ ∀u v x y. u hrat_lt x ∧ v hrat_lt y ⇒ u hrat_mul v hrat_lt x hrat_mul y

⊢ ∀x y. x hrat_lt y ⇒ x ≠ y

⊢ ∀x y. x hrat_mul hrat_inv y hrat_lt hrat_1 ⇔ x hrat_lt y

⊢ ∀x y z. x hrat_add z hrat_lt y hrat_add z ⇔ x hrat_lt y

⊢ ∀x. ¬(x hrat_lt x)

⊢ ∀x y z. x hrat_mul z hrat_lt y hrat_mul z ⇔ x hrat_lt y

⊢ ∀x y. x hrat_mul y hrat_lt x ⇔ y hrat_lt hrat_1

⊢ ∀x y. (x = y) ∨ x hrat_lt y ∨ y hrat_lt x

⊢ ∀x y z. x hrat_lt y ∧ y hrat_lt z ⇒ x hrat_lt z

⊢ ∀x y. x hrat_lt y ⇒ ∃z. x hrat_lt z ∧ z hrat_lt y

⊢ ∀x. x hrat_mul hrat_1 = x

⊢ ∀x. x hrat_mul hrat_inv x = hrat_1

⊢ ∀x y z. (x hrat_add y) hrat_mul z = x hrat_mul z hrat_add y hrat_mul z

⊢ ∀x. ∃y. x hrat_lt y

⊢ ∀X Y Z. X hreal_add (Y hreal_add Z) = X hreal_add Y hreal_add Z

⊢ ∀X Y. isacut (λw. ∃x y. (w = x hrat_add y) ∧ cut X x ∧ cut Y y)

⊢ ∀X Y. X hreal_add Y = Y hreal_add X

⊢ ∀X Y. (X = Y) ∨ (∃D. Y = X hreal_add D) ∨ ∃D. X = Y hreal_add D

⊢ ∀x y. x ≠ x hreal_add y

⊢ ∀x y. x hreal_add y ≠ x

⊢ ∀x y z. (x hreal_add y = x hreal_add z) ⇔ (y = z)

⊢ ∀X. isacut
        (λw. ∃d. d hrat_lt hrat_1 ∧ ∀x. cut X x ⇒ w hrat_mul x hrat_lt d)

⊢ ∀X Y Z.
    X hreal_mul (Y hreal_add Z) = X hreal_mul Y hreal_add X hreal_mul Z

⊢ ∀X Y. X hreal_lt Y ⇔ ∃D. Y = X hreal_add D

⊢ ∀x1 x2 y1 y2.
    x1 hreal_lt y1 ∧ x2 hreal_lt y2 ⇒
    x1 hreal_add x2 hreal_lt y1 hreal_add y2

⊢ ∀x y. x hreal_lt x hreal_add y

⊢ ∀x y. ¬(x hreal_add y hreal_lt x)

⊢ ∀x y. x hreal_lt y ⇒ ¬(y hreal_lt x)

⊢ ∀x y z. x hreal_add y hreal_lt x hreal_add z ⇔ y hreal_lt z

⊢ ∀X Y. X hreal_lt Y ⇒ ∃x. ¬cut X x ∧ cut Y x

⊢ ∀x y. x hreal_lt y ⇒ x ≠ y

⊢ ∀x. ¬(x hreal_lt x)

⊢ ∀X Y. (X = Y) ∨ X hreal_lt Y ∨ Y hreal_lt X

⊢ ∀X Y Z. X hreal_mul (Y hreal_mul Z) = X hreal_mul Y hreal_mul Z

⊢ ∀X Y. isacut (λw. ∃x y. (w = x hrat_mul y) ∧ cut X x ∧ cut Y y)

⊢ ∀X. hreal_1 hreal_mul X = X

⊢ ∀X. hreal_inv X hreal_mul X = hreal_1

⊢ ∀X Y. X hreal_mul Y = Y hreal_mul X

⊢ ∀X Y. X hreal_add Y ≠ X

⊢ ∀x y z.
    (x hreal_add y) hreal_mul z = x hreal_mul z hreal_add y hreal_mul z

⊢ ∀X Y. X hreal_lt Y ⇒ (Y hreal_sub X hreal_add X = Y)

⊢ ∀X Y. X hreal_lt Y ⇒ isacut (λw. ∃x. ¬cut X x ∧ cut Y (x hrat_add w))

⊢ ∀P. (∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒
      ∀Y. (∃X. P X ∧ Y hreal_lt X) ⇔ Y hreal_lt hreal_sup P

⊢ ∀P. (∃X. P X) ∧ (∃Y. ∀X. P X ⇒ X hreal_lt Y) ⇒
      isacut (λw. ∃X. P X ∧ cut X w)

⊢ ∀h. isacut (cut_of_hrat h)

⊢ ¬(treal_1 treal_eq treal_0)

⊢ ∀x y z. x treal_add (y treal_add z) = x treal_add y treal_add z

⊢ ∀x. treal_0 treal_add x treal_eq x

⊢ ∀x. treal_neg x treal_add x treal_eq treal_0

⊢ ∀x y. x treal_add y = y treal_add x

⊢ ∀x1 x2 y1 y2.
    x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒
    x1 treal_add y1 treal_eq x2 treal_add y2

⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ x1 treal_add y treal_eq x2 treal_add y

⊢ (∀h. hreal_of_treal (treal_of_hreal h) = h) ∧
  ∀r. treal_0 treal_lt r ⇔ treal_of_hreal (hreal_of_treal r) treal_eq r

⊢ ∀h i. h treal_eq i ⇒ (hreal_of_treal h = hreal_of_treal i)

⊢ ∀p q. (p = q) ⇒ p treal_eq q

⊢ ∀p q. p treal_eq q ⇔ ($treal_eq p = $treal_eq q)

⊢ ∀x. x treal_eq x

⊢ ∀x y. x treal_eq y ⇔ y treal_eq x

⊢ ∀x y z. x treal_eq y ∧ y treal_eq z ⇒ x treal_eq z

⊢ treal_inv treal_0 treal_eq treal_0

⊢ ∀x1 x2. x1 treal_eq x2 ⇒ treal_inv x1 treal_eq treal_inv x2

⊢ ∀h i. h hreal_lt i ⇒ treal_of_hreal h treal_lt treal_of_hreal i

⊢ ∀x y z.
    x treal_mul (y treal_add z) = x treal_mul y treal_add x treal_mul z

⊢ ∀x y z. y treal_lt z ⇒ x treal_add y treal_lt x treal_add z

⊢ ∀x y.
    treal_0 treal_lt x ∧ treal_0 treal_lt y ⇒
    treal_0 treal_lt x treal_mul y

⊢ ∀x. ¬(x treal_lt x)

⊢ ∀x y. x treal_eq y ∨ x treal_lt y ∨ y treal_lt x

⊢ ∀x y z. x treal_lt y ∧ y treal_lt z ⇒ x treal_lt z

⊢ ∀x1 x2 y1 y2.
    x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒ (x1 treal_lt y1 ⇔ x2 treal_lt y2)

⊢ ∀x y1 y2. y1 treal_eq y2 ⇒ (x treal_lt y1 ⇔ x treal_lt y2)

⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ (x1 treal_lt y ⇔ x2 treal_lt y)

⊢ ∀x y z. x treal_mul (y treal_mul z) = x treal_mul y treal_mul z

⊢ ∀x. treal_1 treal_mul x treal_eq x

⊢ ∀x. ¬(x treal_eq treal_0) ⇒ treal_inv x treal_mul x treal_eq treal_1

⊢ ∀x y. x treal_mul y = y treal_mul x

⊢ ∀x1 x2 y1 y2.
    x1 treal_eq x2 ∧ y1 treal_eq y2 ⇒
    x1 treal_mul y1 treal_eq x2 treal_mul y2

⊢ ∀x1 x2 y. x1 treal_eq x2 ⇒ x1 treal_mul y treal_eq x2 treal_mul y

⊢ ∀x1 x2. x1 treal_eq x2 ⇒ treal_neg x1 treal_eq treal_neg x2