Theory "hreal"

Parents hrat

Signature

Type	Arity
hreal	0
Constant	Type
cut	:hreal -> hrat -> bool
cut_of_hrat	:hrat -> hrat -> bool
hrat_lt	:hrat -> hrat -> bool
hreal	:(hrat -> bool) -> hreal
hreal_1	:hreal
hreal_add	:hreal -> hreal -> hreal
hreal_inv	:hreal -> hreal
hreal_lt	:hreal -> hreal -> bool
hreal_mul	:hreal -> hreal -> hreal
hreal_sub	:hreal -> hreal -> hreal
hreal_sup	:(hreal -> bool) -> hreal
isacut	:(hrat -> bool) -> bool

Definitions

isacut

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

hreal_tybij

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

hreal_TY_DEF

⊢ ∃rep. TYPE_DEFINITION isacut rep

hreal_sup

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

hreal_sub

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

hreal_mul

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

hreal_lt

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

hreal_inv

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

hreal_add

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

hreal_1

⊢ hreal_1 = hreal (cut_of_hrat hrat_1)

hrat_lt

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

cut_of_hrat

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

Theorems

ISACUT_HRAT

⊢ ∀h. isacut (cut_of_hrat h)

HREAL_SUP_ISACUT

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

HREAL_SUP

⊢ ∀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

HREAL_SUB_ISACUT

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

HREAL_SUB_ADD

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

HREAL_NOZERO

⊢ ∀X Y. X hreal_add Y ≠ X

HREAL_MUL_SYM

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

HREAL_MUL_LINV

⊢ ∀X. hreal_inv X hreal_mul X = hreal_1

HREAL_MUL_LID

⊢ ∀X. hreal_1 hreal_mul X = X

HREAL_MUL_ISACUT

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

HREAL_MUL_ASSOC

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

HREAL_LT_TOTAL

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

HREAL_LT_LEMMA

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

HREAL_LT

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

HREAL_LDISTRIB

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

HREAL_INV_ISACUT

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

HREAL_ADD_TOTAL

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

HREAL_ADD_SYM

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

HREAL_ADD_ISACUT

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

HREAL_ADD_ASSOC

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

HRAT_UP

⊢ ∀x. ∃y. hrat_lt x y

HRAT_RDISTRIB

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

HRAT_MUL_RINV

⊢ ∀x. x hrat_mul hrat_inv x = hrat_1

HRAT_MUL_RID

⊢ ∀x. x hrat_mul hrat_1 = x

HRAT_MEAN

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

HRAT_LT_TRANS

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

HRAT_LT_TOTAL

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

HRAT_LT_RMUL1

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

HRAT_LT_RMUL

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

HRAT_LT_REFL

⊢ ∀x. ¬hrat_lt x x

HRAT_LT_RADD

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

HRAT_LT_R1

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

HRAT_LT_NE

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

HRAT_LT_MUL2

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

HRAT_LT_LMUL1

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

HRAT_LT_LMUL

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

HRAT_LT_LADD

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

HRAT_LT_L1

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

HRAT_LT_GT

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

HRAT_LT_ANTISYM

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

HRAT_LT_ADDR

⊢ ∀x y. hrat_lt y (x hrat_add y)

HRAT_LT_ADDL

⊢ ∀x y. hrat_lt x (x hrat_add y)

HRAT_LT_ADD2

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

HRAT_INV_MUL

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

HRAT_GT_LMUL1

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

HRAT_GT_L1

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

HRAT_EQ_LMUL

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

HRAT_EQ_LADD

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

HRAT_DOWN2

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

HRAT_DOWN

⊢ ∀x. ∃y. hrat_lt y x

EQUAL_CUTS

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

CUT_UP

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

CUT_UBOUND

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

CUT_STRADDLE

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

CUT_NONEMPTY

⊢ ∀X. ∃x. cut X x

CUT_NEARTOP_MUL

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

CUT_NEARTOP_ADD

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

CUT_ISACUT

⊢ ∀X. isacut (cut X)

CUT_DOWN

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

CUT_BOUNDED

⊢ ∀X. ∃x. ¬cut X x