- num_not_infty
-
|- ∀n. &n ≠ NegInf ∧ &n ≠ PosInf
- extreal_not_infty
-
|- ∀x. Normal x ≠ NegInf ∧ Normal x ≠ PosInf
- extreal_eq_zero
-
|- ∀x. (Normal x = 0) ⇔ (x = 0)
- extreal_cases
-
|- ∀x. (x = NegInf) ∨ (x = PosInf) ∨ ∃r. x = Normal r
- mono_increasing_converges_to_sup
-
|- ∀f r. mono_increasing f ∧ f --> r ⇒ (r = sup (IMAGE f 𝕌(:num)))
- mono_decreasing_suc
-
|- ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n
- mono_increasing_suc
-
|- ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)
- LOGR_MONO_LE_IMP
-
|- ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y
- LOGR_MONO_LE
-
|- ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)
- POW_NEG_ODD
-
|- ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
- POW_POS_EVEN
-
|- ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
- REAL_LE_RDIV_EQ_NEG
-
|- ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)
- REAL_LT_RDIV_EQ_NEG
-
|- ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)
- REAL_LT_RMUL_NEG_0_NEG
-
|- ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x
- REAL_LT_LMUL_NEG_0_NEG
-
|- ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y
- REAL_LT_RMUL_NEG_0
-
|- ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0
- REAL_LT_LMUL_NEG_0
-
|- ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0
- REAL_LT_RMUL_0_NEG
-
|- ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0
- REAL_LT_LMUL_0_NEG
-
|- ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0
- extreal_abs_def
-
|- (abs (Normal x) = Normal (abs x)) ∧ (abs NegInf = PosInf) ∧
(abs PosInf = PosInf)
- extreal_abs_ind
-
|- ∀P. (∀x. P (Normal x)) ∧ P NegInf ∧ P PosInf ⇒ ∀v. P v
- extreal_mul_def
-
|- (NegInf * NegInf = PosInf) ∧ (NegInf * PosInf = NegInf) ∧
(PosInf * NegInf = NegInf) ∧ (PosInf * PosInf = PosInf) ∧
(Normal x * NegInf =
if x = 0 then Normal 0 else if 0 < x then NegInf else PosInf) ∧
(NegInf * Normal y =
if y = 0 then Normal 0 else if 0 < y then NegInf else PosInf) ∧
(Normal x * PosInf =
if x = 0 then Normal 0 else if 0 < x then PosInf else NegInf) ∧
(PosInf * Normal y =
if y = 0 then Normal 0 else if 0 < y then PosInf else NegInf) ∧
(Normal x * Normal y = Normal (x * y))
- extreal_mul_ind
-
|- ∀P.
P NegInf NegInf ∧ P NegInf PosInf ∧ P PosInf NegInf ∧ P PosInf PosInf ∧
(∀x. P (Normal x) NegInf) ∧ (∀y. P NegInf (Normal y)) ∧
(∀x. P (Normal x) PosInf) ∧ (∀y. P PosInf (Normal y)) ∧
(∀x y. P (Normal x) (Normal y)) ⇒
∀v v1. P v v1
- extreal_le_def
-
|- (Normal x ≤ Normal y ⇔ x ≤ y) ∧ (NegInf ≤ a ⇔ T) ∧ (PosInf ≤ PosInf ⇔ T) ∧
(Normal v2 ≤ PosInf ⇔ T) ∧ (PosInf ≤ NegInf ⇔ F) ∧
(Normal v3 ≤ NegInf ⇔ F) ∧ (PosInf ≤ Normal v5 ⇔ F)
- extreal_le_ind
-
|- ∀P.
(∀x y. P (Normal x) (Normal y)) ∧ (∀a. P NegInf a) ∧ P PosInf PosInf ∧
(∀v2. P (Normal v2) PosInf) ∧ P PosInf NegInf ∧
(∀v3. P (Normal v3) NegInf) ∧ (∀v5. P PosInf (Normal v5)) ⇒
∀v v1. P v v1
- extreal_sub_def
-
|- (Normal x − Normal y = Normal (x − y)) ∧ (PosInf − a = PosInf) ∧
(NegInf − PosInf = NegInf) ∧ (Normal v2 − PosInf = NegInf) ∧
(NegInf − NegInf = PosInf) ∧ (NegInf − Normal v5 = NegInf) ∧
(Normal v3 − NegInf = PosInf)
- extreal_sub_ind
-
|- ∀P.
(∀x y. P (Normal x) (Normal y)) ∧ (∀a. P PosInf a) ∧ P NegInf PosInf ∧
(∀v2. P (Normal v2) PosInf) ∧ P NegInf NegInf ∧
(∀v5. P NegInf (Normal v5)) ∧ (∀v3. P (Normal v3) NegInf) ⇒
∀v v1. P v v1
- extreal_add_def
-
|- (Normal x + Normal y = Normal (x + y)) ∧ (PosInf + a = PosInf) ∧
(NegInf + PosInf = PosInf) ∧ (Normal v2 + PosInf = PosInf) ∧
(NegInf + NegInf = NegInf) ∧ (NegInf + Normal v5 = NegInf) ∧
(Normal v3 + NegInf = NegInf)
- extreal_add_ind
-
|- ∀P.
(∀x y. P (Normal x) (Normal y)) ∧ (∀a. P PosInf a) ∧ P NegInf PosInf ∧
(∀v2. P (Normal v2) PosInf) ∧ P NegInf NegInf ∧
(∀v5. P NegInf (Normal v5)) ∧ (∀v3. P (Normal v3) NegInf) ⇒
∀v v1. P v v1
- normal_real
-
|- ∀x. x ≠ NegInf ∧ x ≠ PosInf ⇒ (Normal (real x) = x)
- real_normal
-
|- ∀x. real (Normal x) = x
- extreal_induction
-
|- ∀P. P NegInf ∧ P PosInf ∧ (∀r. P (Normal r)) ⇒ ∀e. P e
- extreal_Axiom
-
|- ∀f0 f1 f2.
∃fn. (fn NegInf = f0) ∧ (fn PosInf = f1) ∧ ∀a. fn (Normal a) = f2 a
- extreal_nchotomy
-
|- ∀ee. (ee = NegInf) ∨ (ee = PosInf) ∨ ∃r. ee = Normal r
- extreal_case_cong
-
|- ∀M M' v v1 f.
(M = M') ∧ ((M' = NegInf) ⇒ (v = v')) ∧ ((M' = PosInf) ⇒ (v1 = v1')) ∧
(∀a. (M' = Normal a) ⇒ (f a = f' a)) ⇒
(extreal_CASE M v v1 f = extreal_CASE M' v' v1' f')
- extreal_distinct
-
|- NegInf ≠ PosInf ∧ (∀a. NegInf ≠ Normal a) ∧ ∀a. PosInf ≠ Normal a
- datatype_extreal
-
|- DATATYPE (extreal NegInf PosInf Normal)
- extreal_11
-
|- ∀a a'. (Normal a = Normal a') ⇔ (a = a')
- mul_rzero
-
|- ∀x. x * 0 = 0
- mul_lzero
-
|- ∀x. 0 * x = 0
- mul_rone
-
|- ∀x. x * 1 = x
- mul_lone
-
|- ∀x. 1 * x = x
- entire
-
|- ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)
- extreal_lt_eq
-
|- ∀x y. Normal x < Normal y ⇔ x < y
- le_refl
-
|- ∀x. x ≤ x
- lt_refl
-
|- ∀x. ¬(x < x)
- le_infty
-
|- (∀x. NegInf ≤ x ∧ x ≤ PosInf) ∧ (∀x. x ≤ NegInf ⇔ (x = NegInf)) ∧
∀x. PosInf ≤ x ⇔ (x = PosInf)
- lt_infty
-
|- ∀x y.
NegInf < Normal y ∧ Normal y < PosInf ∧ NegInf < PosInf ∧ ¬(x < NegInf) ∧
¬(PosInf < x) ∧ (x ≠ PosInf ⇔ x < PosInf) ∧ (x ≠ NegInf ⇔ NegInf < x)
- lt_imp_le
-
|- ∀x y. x < y ⇒ x ≤ y
- lt_imp_ne
-
|- ∀x y. x < y ⇒ x ≠ y
- le_trans
-
|- ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
- lt_trans
-
|- ∀x y z. x < y ∧ y < z ⇒ x < z
- let_trans
-
|- ∀x y z. x ≤ y ∧ y < z ⇒ x < z
- le_antisym
-
|- ∀x y. x ≤ y ∧ y ≤ x ⇔ (x = y)
- lt_antisym
-
|- ∀x y. ¬(x < y ∧ y < x)
- lte_trans
-
|- ∀x y z. x < y ∧ y ≤ z ⇒ x < z
- le_total
-
|- ∀x y. x ≤ y ∨ y ≤ x
- lt_total
-
|- ∀x y. (x = y) ∨ x < y ∨ y < x
- le_01
-
|- 0 ≤ 1
- lt_01
-
|- 0 < 1
- ne_01
-
|- 0 ≠ 1
- le_02
-
|- 0 ≤ 2
- lt_02
-
|- 0 < 2
- ne_02
-
|- 0 ≠ 2
- le_num
-
|- ∀n. 0 ≤ &n
- lt_le
-
|- ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
- le_lt
-
|- ∀x y. x ≤ y ⇔ x < y ∨ (x = y)
- le_neg
-
|- ∀x y. -x ≤ -y ⇔ y ≤ x
- lt_neg
-
|- ∀x y. -x < -y ⇔ y < x
- le_add
-
|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
- lt_add
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
- let_add
-
|- ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
- lte_add
-
|- ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
- le_add2
-
|- ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
- lt_add2
-
|- ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
- let_add2
-
|- ∀w x y z. w ≠ NegInf ∧ w ≠ PosInf ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
- let_add2_alt
-
|- ∀w x y z. x ≠ NegInf ∧ x ≠ PosInf ∧ w ≤ x ∧ y < z ⇒ w + y < x + z
- le_addr
-
|- ∀x y. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x ≤ x + y ⇔ 0 ≤ y)
- le_addr_imp
-
|- ∀x y. 0 ≤ y ⇒ x ≤ x + y
- le_ladd
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x + y ≤ x + z ⇔ y ≤ z)
- le_radd
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y + x ≤ z + x ⇔ y ≤ z)
- le_radd_imp
-
|- ∀x y z. y ≤ z ⇒ y + x ≤ z + x
- le_ladd_imp
-
|- ∀x y z. y ≤ z ⇒ x + y ≤ x + z
- lt_ladd
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x + y < x + z ⇔ y < z)
- lt_radd
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y + x < z + x ⇔ y < z)
- lt_addl
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (y < x + y ⇔ 0 < x)
- le_lneg
-
|- ∀x y. -x ≤ y ⇔ 0 ≤ x + y
- le_mul
-
|- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
- let_mul
-
|- ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
- lte_mul
-
|- ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
- le_mul_neg
-
|- ∀x y. x ≤ 0 ∧ y ≤ 0 ⇒ 0 ≤ x * y
- mul_le
-
|- ∀x y. 0 ≤ x ∧ y ≤ 0 ⇒ x * y ≤ 0
- lt_mul
-
|- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y
- lt_mul_neg
-
|- ∀x y. x < 0 ∧ y < 0 ⇒ 0 < x * y
- mul_lt
-
|- ∀x y. 0 < x ∧ y < 0 ⇒ x * y < 0
- mul_let
-
|- ∀x y. 0 ≤ x ∧ y < 0 ⇒ x * y ≤ 0
- mul_lte
-
|- ∀x y. 0 < x ∧ y ≤ 0 ⇒ x * y ≤ 0
- le_rmul_imp
-
|- ∀x y z. 0 < z ∧ x ≤ y ⇒ x * z ≤ y * z
- le_lmul_imp
-
|- ∀x y z. 0 ≤ z ∧ x ≤ y ⇒ z * x ≤ z * y
- lt_rmul
-
|- ∀x y z. 0 < z ∧ z ≠ PosInf ⇒ (x * z < y * z ⇔ x < y)
- lt_lmul
-
|- ∀x y z. 0 < x ∧ x ≠ PosInf ⇒ (x * y < x * z ⇔ y < z)
- lt_mul2
-
|- ∀x1 x2 y1 y2.
0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≠ PosInf ∧ y1 ≠ PosInf ∧ x1 < x2 ∧ y1 < y2 ⇒
x1 * y1 < x2 * y2
- abs_pos
-
|- ∀x. 0 ≤ abs x
- abs_refl
-
|- ∀x. (abs x = x) ⇔ 0 ≤ x
- abs_bounds
-
|- ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k
- abs_bounds_lt
-
|- ∀x k. abs x < k ⇔ -k < x ∧ x < k
- add_comm
-
|- ∀x y. x + y = y + x
- add_assoc
-
|- ∀x y z. x + (y + z) = x + y + z
- add_not_infty
-
|- ∀x y.
(x ≠ NegInf ∧ y ≠ NegInf ⇒ x + y ≠ NegInf) ∧
(x ≠ PosInf ∧ y ≠ PosInf ⇒ x + y ≠ PosInf)
- add_rzero
-
|- ∀x. x + 0 = x
- add_lzero
-
|- ∀x. 0 + x = x
- add_infty
-
|- (∀x. (x + PosInf = PosInf) ∧ (PosInf + x = PosInf)) ∧
∀x. x ≠ PosInf ⇒ (x + NegInf = NegInf) ∧ (NegInf + x = NegInf)
- EXTREAL_EQ_LADD
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ ((x + y = x + z) ⇔ (y = z))
- sub_rzero
-
|- ∀x. x − 0 = x
- sub_lzero
-
|- ∀x. 0 − x = -x
- sub_le_imp
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ∧ y ≤ z + x ⇒ y − x ≤ z
- sub_le_imp2
-
|- ∀x y z. y ≠ NegInf ∧ y ≠ PosInf ∧ y ≤ z + x ⇒ y − x ≤ z
- le_sub_imp
-
|- ∀x y z. y + x ≤ z ⇒ y ≤ z − x
- lt_sub_imp
-
|- ∀x y z. y + x < z ⇒ y < z − x
- sub_lt_imp
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ∧ y < z + x ⇒ y − x < z
- sub_lt_imp2
-
|- ∀x y z. z ≠ NegInf ∧ z ≠ PosInf ∧ y < z + x ⇒ y − x < z
- sub_zero_lt
-
|- ∀x y. x < y ⇒ 0 < y − x
- sub_zero_lt2
-
|- ∀x y. x ≠ NegInf ∧ x ≠ PosInf ∧ 0 < y − x ⇒ x < y
- sub_lt_zero
-
|- ∀x y. x < y ⇒ x − y < 0
- sub_lt_zero2
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ∧ x − y < 0 ⇒ x < y
- sub_zero_le
-
|- ∀x y. x ≤ y ⇔ 0 ≤ y − x
- sub_le_zero
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (x ≤ y ⇔ x − y ≤ 0)
- le_sub_eq
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y ≤ z − x ⇔ y + x ≤ z)
- le_sub_eq2
-
|- ∀x y z.
z ≠ NegInf ∧ z ≠ PosInf ∧ x ≠ NegInf ∧ y ≠ NegInf ⇒
(y ≤ z − x ⇔ y + x ≤ z)
- sub_le_eq
-
|- ∀x y z. x ≠ NegInf ∧ x ≠ PosInf ⇒ (y − x ≤ z ⇔ y ≤ z + x)
- sub_le_eq2
-
|- ∀x y z.
y ≠ NegInf ∧ y ≠ PosInf ∧ x ≠ NegInf ∧ z ≠ NegInf ⇒
(y − x ≤ z ⇔ y ≤ z + x)
- sub_le_switch
-
|- ∀x y z.
x ≠ NegInf ∧ x ≠ PosInf ∧ z ≠ NegInf ∧ z ≠ PosInf ⇒
(y − x ≤ z ⇔ y − z ≤ x)
- sub_le_switch2
-
|- ∀x y z.
x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ⇒
(y − x ≤ z ⇔ y − z ≤ x)
- lt_sub
-
|- ∀x y z. z ≠ NegInf ∧ z ≠ PosInf ⇒ (y + x < z ⇔ y < z − x)
- sub_add2
-
|- ∀x y. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x + (y − x) = y)
- add_sub
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (x + y − y = x)
- add_sub2
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (y + x − y = x)
- sub_add
-
|- ∀x y. y ≠ NegInf ∧ y ≠ PosInf ⇒ (x − y + y = x)
- extreal_sub_add
-
|- ∀x y. x − y = x + -y
- sub_0
-
|- ∀x y. (x − y = 0) ⇒ (x = y)
- neg_neg
-
|- ∀x. - -x = x
- neg_0
-
|- -0 = 0
- neg_eq0
-
|- ∀x. (-x = 0) ⇔ (x = 0)
- eq_neg
-
|- ∀x y. (-x = -y) ⇔ (x = y)
- neg_minus1
-
|- ∀x. -x = -1 * x
- sub_rneg
-
|- ∀x y. x − -y = x + y
- sub_lneg
-
|- ∀x y.
x ≠ NegInf ∧ y ≠ NegInf ∨ x ≠ PosInf ∧ y ≠ PosInf ⇒ (-x − y = -(x + y))
- neg_sub
-
|- ∀x y.
x ≠ NegInf ∧ x ≠ PosInf ∨ y ≠ NegInf ∧ y ≠ PosInf ⇒ (-(x − y) = y − x)
- sub_not_infty
-
|- ∀x y.
(x ≠ NegInf ∧ y ≠ PosInf ⇒ x − y ≠ NegInf) ∧
(x ≠ PosInf ∧ y ≠ NegInf ⇒ x − y ≠ PosInf)
- le_lsub_imp
-
|- ∀x y z. y ≤ z ⇒ x − z ≤ x − y
- eq_sub_ladd_normal
-
|- ∀x y z. (x = y − Normal z) ⇔ (x + Normal z = y)
- eq_sub_radd
-
|- ∀x y z. y ≠ NegInf ∧ y ≠ PosInf ⇒ ((x − y = z) ⇔ (x = z + y))
- eq_sub_ladd
-
|- ∀x y z. z ≠ NegInf ∧ z ≠ PosInf ⇒ ((x = y − z) ⇔ (x + z = y))
- eq_sub_switch
-
|- ∀x y z. (x = Normal z − y) ⇔ (y = Normal z − x)
- eq_add_sub_switch
-
|- ∀a b c d.
b ≠ NegInf ∧ b ≠ PosInf ∧ c ≠ NegInf ∧ c ≠ PosInf ⇒
((a + b = c + d) ⇔ (a − c = d − b))
- sub_refl
-
|- ∀x. x ≠ NegInf ∧ x ≠ PosInf ⇒ (x − x = 0)
- mul_comm
-
|- ∀x y. x * y = y * x
- mul_assoc
-
|- ∀x y z. x * (y * z) = x * y * z
- mul_not_infty
-
|- (∀c y. 0 ≤ c ∧ y ≠ NegInf ⇒ Normal c * y ≠ NegInf) ∧
(∀c y. 0 ≤ c ∧ y ≠ PosInf ⇒ Normal c * y ≠ PosInf) ∧
(∀c y. c ≤ 0 ∧ y ≠ NegInf ⇒ Normal c * y ≠ PosInf) ∧
∀c y. c ≤ 0 ∧ y ≠ PosInf ⇒ Normal c * y ≠ NegInf
- mul_not_infty2
-
|- ∀x y.
x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ⇒
x * y ≠ NegInf ∧ x * y ≠ PosInf
- add_ldistrib_pos
-
|- ∀x y z. 0 ≤ y ∧ 0 ≤ z ⇒ (x * (y + z) = x * y + x * z)
- add_ldistrib_neg
-
|- ∀x y z. y ≤ 0 ∧ z ≤ 0 ⇒ (x * (y + z) = x * y + x * z)
- add_ldistrib_normal
-
|- ∀x y z.
y ≠ PosInf ∧ z ≠ PosInf ∨ y ≠ NegInf ∧ z ≠ NegInf ⇒
(Normal x * (y + z) = Normal x * y + Normal x * z)
- add_ldistrib_normal2
-
|- ∀x y z. 0 ≤ x ⇒ (Normal x * (y + z) = Normal x * y + Normal x * z)
- add_rdistrib_normal
-
|- ∀x y z.
y ≠ PosInf ∧ z ≠ PosInf ∨ y ≠ NegInf ∧ z ≠ NegInf ⇒
((y + z) * Normal x = y * Normal x + z * Normal x)
- add_rdistrib_normal2
-
|- ∀x y z. 0 ≤ x ⇒ ((y + z) * Normal x = y * Normal x + z * Normal x)
- add_ldistrib
-
|- ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ (x * (y + z) = x * y + x * z)
- add_rdistrib
-
|- ∀x y z. 0 ≤ y ∧ 0 ≤ z ∨ y ≤ 0 ∧ z ≤ 0 ⇒ ((y + z) * x = y * x + z * x)
- mul_lneg
-
|- ∀x y. -x * y = -(x * y)
- mul_rneg
-
|- ∀x y. x * -y = -(x * y)
- neg_mul2
-
|- ∀x y. -x * -y = x * y
- add2_sub2
-
|- ∀a b c d.
b ≠ PosInf ∧ d ≠ PosInf ∨ b ≠ NegInf ∧ d ≠ NegInf ⇒
(a − b + (c − d) = a + c − (b + d))
- sub_ldistrib
-
|- ∀x y z.
x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ∧ z ≠ NegInf ∧
z ≠ PosInf ⇒
(x * (y − z) = x * y − x * z)
- sub_rdistrib
-
|- ∀x y z.
x ≠ NegInf ∧ x ≠ PosInf ∧ y ≠ NegInf ∧ y ≠ PosInf ∧ z ≠ NegInf ∧
z ≠ PosInf ⇒
((x − y) * z = x * z − y * z)
- extreal_div_eq
-
|- ∀x y. Normal x / Normal y = Normal (x / y)
- inv_one
-
|- inv 1 = 1
- inv_1over
-
|- ∀x. inv x = 1 / x
- div_one
-
|- ∀x. x / 1 = x
- inv_pos
-
|- ∀x. 0 < x ∧ x ≠ PosInf ⇒ 0 < 1 / x
- rinv_uniq
-
|- ∀x y. (x * y = 1) ⇒ (y = inv x)
- linv_uniq
-
|- ∀x y. (x * y = 1) ⇒ (x = inv y)
- le_rdiv
-
|- ∀x y z. 0 < x ⇒ (y * Normal x ≤ z ⇔ y ≤ z / Normal x)
- le_ldiv
-
|- ∀x y z. 0 < x ⇒ (y ≤ z * Normal x ⇔ y / Normal x ≤ z)
- lt_rdiv
-
|- ∀x y z. 0 < z ⇒ (x < y / Normal z ⇔ x * Normal z < y)
- lt_ldiv
-
|- ∀x y z. 0 < z ⇒ (x / Normal z < y ⇔ x < y * Normal z)
- lt_rdiv_neg
-
|- ∀x y z. z < 0 ⇒ (y / Normal z < x ⇔ x * Normal z < y)
- div_add
-
|- ∀x y z. x ≠ NegInf ∧ y ≠ NegInf ∧ z ≠ 0 ⇒ (x / z + y / z = (x + y) / z)
- le_inv
-
|- ∀x. 0 ≤ x ⇒ 0 ≤ inv x
- pow_0
-
|- ∀x. x pow 0 = 1
- pow_1
-
|- ∀x. x pow 1 = x
- pow_2
-
|- ∀x. x pow 2 = x * x
- pow_zero
-
|- ∀n x. (x pow SUC n = 0) ⇔ (x = 0)
- pow_zero_imp
-
|- ∀n x. (x pow n = 0) ⇒ (x = 0)
- le_pow2
-
|- ∀x. 0 ≤ x pow 2
- pow_pos_le
-
|- ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n
- pow_pos_lt
-
|- ∀x n. 0 < x ⇒ 0 < x pow n
- pow_le
-
|- ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n
- pow_lt
-
|- ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n
- pow_lt2
-
|- ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n
- pow_le_mono
-
|- ∀x n m. 1 ≤ x ∧ n ≤ m ⇒ x pow n ≤ x pow m
- pow_pos_even
-
|- ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
- pow_neg_odd
-
|- ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
- add_pow2
-
|- ∀x y. (x + y) pow 2 = x pow 2 + y pow 2 + 2 * x * y
- pow_add
-
|- ∀x n m. x pow (n + m) = x pow n * x pow m
- pow_mul
-
|- ∀n x y. (x * y) pow n = x pow n * y pow n
- pow_minus1
-
|- ∀n. -1 pow (2 * n) = 1
- pow_not_infty
-
|- ∀n x. x ≠ NegInf ∧ x ≠ PosInf ⇒ x pow n ≠ NegInf ∧ x pow n ≠ PosInf
- sqrt_pos_le
-
|- ∀x. 0 ≤ x ⇒ 0 ≤ sqrt x
- sqrt_pos_lt
-
|- ∀x. 0 < x ⇒ 0 < sqrt x
- pow2_sqrt
-
|- ∀x. 0 ≤ x ⇒ (sqrt (x pow 2) = x)
- sqrt_pow2
-
|- ∀x. (sqrt x pow 2 = x) ⇔ 0 ≤ x
- sqrt_mono_le
-
|- ∀x y. 0 ≤ x ∧ x ≤ y ⇒ sqrt x ≤ sqrt y
- logr_not_infty
-
|- ∀x b. x ≠ NegInf ∧ x ≠ PosInf ⇒ logr b x ≠ NegInf ∧ logr b x ≠ PosInf
- half_between
-
|- (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1
- thirds_between
-
|- ((0 < 1 / 3 ∧ 1 / 3 < 1) ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧
(0 ≤ 1 / 3 ∧ 1 / 3 ≤ 1) ∧ 0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1
- half_cancel
-
|- 2 * (1 / 2) = 1
- third_cancel
-
|- 3 * (1 / 3) = 1
- fourth_cancel
-
|- 4 * (1 / 4) = 1
- quotient_normal
-
|- ∀n m. &n / &m = Normal (&n / &m)
- ext_mono_increasing_suc
-
|- ∀f. mono_increasing f ⇔ ∀n. f n ≤ f (SUC n)
- ext_mono_decreasing_suc
-
|- ∀f. mono_decreasing f ⇔ ∀n. f (SUC n) ≤ f n
- EXTREAL_ARCH
-
|- ∀x. 0 < x ⇒ ∀y. y ≠ PosInf ⇒ ∃n. y < &n * x
- SIMP_REAL_ARCH
-
|- ∀x. ∃n. x ≤ &n
- SIMP_REAL_ARCH_NEG
-
|- ∀x. ∃n. -&n ≤ x
- SIMP_EXTREAL_ARCH
-
|- ∀x. x ≠ PosInf ⇒ ∃n. x ≤ &n
- REAL_ARCH_POW
-
|- ∀x. ∃n. x < 2 pow n
- EXTREAL_ARCH_POW
-
|- ∀x. x ≠ PosInf ⇒ ∃n. x < 2 pow n
- EXTREAL_ARCH_POW_INV
-
|- ∀e. 0 < e ⇒ ∃n. Normal ((1 / 2) pow n) < e
- REAL_LE_MUL_EPSILON
-
|- ∀x y. (∀z. 0 < z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
- le_epsilon
-
|- ∀x y. (∀e. 0 < e ∧ e ≠ PosInf ⇒ x ≤ y + e) ⇒ x ≤ y
- le_mul_epsilon
-
|- ∀x y. (∀z. 0 ≤ z ∧ z < 1 ⇒ z * x ≤ y) ⇒ x ≤ y
- EXTREAL_SUM_IMAGE_THM
-
|- ∀f.
(SIGMA f ∅ = 0) ∧
∀e s. FINITE s ⇒ (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
- EXTREAL_SUM_IMAGE_NOT_NEG_INF
-
|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒ SIGMA f s ≠ NegInf
- EXTREAL_SUM_IMAGE_NOT_POS_INF
-
|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ PosInf) ⇒ SIGMA f s ≠ PosInf
- EXTREAL_SUM_IMAGE_NOT_INFTY
-
|- ∀f s.
(FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒ SIGMA f s ≠ NegInf) ∧
(FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ PosInf) ⇒ SIGMA f s ≠ PosInf)
- EXTREAL_SUM_IMAGE_SING
-
|- ∀f e. SIGMA f {e} = f e
- EXTREAL_SUM_IMAGE_POS
-
|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ SIGMA f s
- EXTREAL_SUM_IMAGE_SPOS
-
|- ∀f s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < SIGMA f s
- EXTREAL_SUM_IMAGE_IF_ELIM
-
|- ∀s P f.
FINITE s ∧ (∀x. x ∈ s ⇒ P x) ⇒
(SIGMA (λx. if P x then f x else 0) s = SIGMA f s)
- EXTREAL_SUM_IMAGE_FINITE_SAME
-
|- ∀s.
FINITE s ⇒
∀f p. p ∈ s ∧ (∀q. q ∈ s ⇒ (f p = f q)) ⇒ (SIGMA f s = &CARD s * f p)
- EXTREAL_SUM_IMAGE_FINITE_CONST
-
|- ∀P. FINITE P ⇒ ∀f x. (∀y. f y = x) ⇒ (SIGMA f P = &CARD P * x)
- EXTREAL_SUM_IMAGE_ZERO
-
|- ∀s. FINITE s ⇒ (SIGMA (λx. 0) s = 0)
- EXTREAL_SUM_IMAGE_0
-
|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (SIGMA f s = 0)
- EXTREAL_SUM_IMAGE_IN_IF
-
|- ∀s. FINITE s ⇒ ∀f. SIGMA f s = SIGMA (λx. if x ∈ s then f x else 0) s
- EXTREAL_SUM_IMAGE_CMUL
-
|- ∀s.
FINITE s ⇒
∀f c.
0 ≤ c ∨ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒
(SIGMA (λx. Normal c * f x) s = Normal c * SIGMA f s)
- EXTREAL_SUM_IMAGE_CMUL2
-
|- ∀s f c.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≠ NegInf) ⇒
(SIGMA (λx. Normal c * f x) s = Normal c * SIGMA f s)
- EXTREAL_SUM_IMAGE_IMAGE
-
|- ∀s.
FINITE s ⇒
∀f'. INJ f' s (IMAGE f' s) ⇒ ∀f. SIGMA f (IMAGE f' s) = SIGMA (f o f') s
- EXTREAL_SUM_IMAGE_DISJOINT_UNION
-
|- ∀s s'.
FINITE s ∧ FINITE s' ∧ DISJOINT s s' ⇒
∀f. SIGMA f (s ∪ s') = SIGMA f s + SIGMA f s'
- EXTREAL_SUM_IMAGE_EQ_CARD
-
|- ∀s. FINITE s ⇒ (SIGMA (λx. if x ∈ s then 1 else 0) s = &CARD s)
- EXTREAL_SUM_IMAGE_INV_CARD_EQ_1
-
|- ∀s.
s ≠ ∅ ∧ FINITE s ⇒ (SIGMA (λx. if x ∈ s then inv (&CARD s) else 0) s = 1)
- EXTREAL_SUM_IMAGE_INTER_NONZERO
-
|- ∀s. FINITE s ⇒ ∀f. SIGMA f (s ∩ (λp. f p ≠ 0)) = SIGMA f s
- EXTREAL_SUM_IMAGE_INTER_ELIM
-
|- ∀s.
FINITE s ⇒
∀f s'. (∀x. x ∉ s' ⇒ (f x = 0)) ⇒ (SIGMA f (s ∩ s') = SIGMA f s)
- EXTREAL_SUM_IMAGE_ZERO_DIFF
-
|- ∀s.
FINITE s ⇒
∀f t. (∀x. x ∈ t ⇒ (f x = 0)) ⇒ (SIGMA f s = SIGMA f (s DIFF t))
- EXTREAL_SUM_IMAGE_MONO
-
|- ∀s. FINITE s ⇒ ∀f f'. (∀x. x ∈ s ⇒ f x ≤ f' x) ⇒ SIGMA f s ≤ SIGMA f' s
- EXTREAL_SUM_IMAGE_MONO_SET
-
|- ∀f s t.
FINITE s ∧ FINITE t ∧ s ⊆ t ∧ (∀x. x ∈ t ⇒ 0 ≤ f x) ⇒
SIGMA f s ≤ SIGMA f t
- EXTREAL_SUM_IMAGE_EQ
-
|- ∀s. FINITE s ⇒ ∀f f'. (∀x. x ∈ s ⇒ (f x = f' x)) ⇒ (SIGMA f s = SIGMA f' s)
- EXTREAL_SUM_IMAGE_POS_MEM_LE
-
|- ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ ∀x. x ∈ s ⇒ f x ≤ SIGMA f s
- EXTREAL_SUM_IMAGE_ADD
-
|- ∀s. FINITE s ⇒ ∀f f'. SIGMA (λx. f x + f' x) s = SIGMA f s + SIGMA f' s
- EXTREAL_SUM_IMAGE_SUB
-
|- ∀s.
FINITE s ⇒
∀f f'.
(∀x. x ∈ s ⇒ f' x ≠ NegInf) ∨ (∀x. x ∈ s ⇒ f' x ≠ PosInf) ⇒
(SIGMA (λx. f x − f' x) s = SIGMA f s − SIGMA f' s)
- EXTREAL_SUM_IMAGE_EXTREAL_SUM_IMAGE
-
|- ∀s s' f.
FINITE s ∧ FINITE s' ⇒
(SIGMA (λx. SIGMA (f x) s') s = SIGMA (λx. f (FST x) (SND x)) (s × s'))
- EXTREAL_SUM_IMAGE_NORMAL
-
|- ∀f s. FINITE s ⇒ (SIGMA (λx. Normal (f x)) s = Normal (SIGMA f s))
- EXTREAL_SUM_IMAGE_IN_IF_ALT
-
|- ∀s f z. FINITE s ⇒ (SIGMA f s = SIGMA (λx. if x ∈ s then f x else z) s)
- EXTREAL_SUM_IMAGE_CROSS_SYM
-
|- ∀f s1 s2.
FINITE s1 ∧ FINITE s2 ⇒
(SIGMA (λ(x,y). f (x,y)) (s1 × s2) = SIGMA (λ(y,x). f (x,y)) (s2 × s1))
- EXTREAL_SUM_IMAGE_COUNT
-
|- ∀f.
(SIGMA f (count 2) = f 0 + f 1) ∧ (SIGMA f (count 3) = f 0 + f 1 + f 2) ∧
(SIGMA f (count 4) = f 0 + f 1 + f 2 + f 3) ∧
(SIGMA f (count 5) = f 0 + f 1 + f 2 + f 3 + f 4)
- le_sup_imp
-
|- ∀p x. p x ⇒ x ≤ sup p
- sup_le
-
|- ∀p x. sup p ≤ x ⇔ ∀y. p y ⇒ y ≤ x
- le_sup
-
|- ∀p x. x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
- sup_eq
-
|- ∀p x. (sup p = x) ⇔ (∀y. p y ⇒ y ≤ x) ∧ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y
- sup_const
-
|- ∀x. sup (λy. y = x) = x
- sup_const_alt
-
|- ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ (x = z)) ⇒ (sup p = z)
- sup_const_over_set
-
|- ∀s k. s ≠ ∅ ⇒ (sup (IMAGE (λx. k) s) = k)
- sup_num
-
|- sup (λx. ∃n. x = &n) = PosInf
- sup_le_sup_imp
-
|- ∀p q. (∀x. p x ⇒ ∃y. q y ∧ x ≤ y) ⇒ sup p ≤ sup q
- sup_mono
-
|- ∀p q. (∀n. p n ≤ q n) ⇒ sup (IMAGE p 𝕌(:num)) ≤ sup (IMAGE q 𝕌(:num))
- sup_suc
-
|- ∀f.
(∀m n. m ≤ n ⇒ f m ≤ f n) ⇒
(sup (IMAGE (λn. f (SUC n)) 𝕌(:num)) = sup (IMAGE f 𝕌(:num)))
- sup_seq
-
|- ∀f l.
mono_increasing f ⇒
(f --> l ⇔ (sup (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l))
- sup_lt_infty
-
|- ∀p. sup p < PosInf ⇒ ∀x. p x ⇒ x < PosInf
- sup_max
-
|- ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ (sup p = z)
- sup_add_mono
-
|- ∀f g.
(∀n. 0 ≤ f n) ∧ (∀n. f n ≤ f (SUC n)) ∧ (∀n. 0 ≤ g n) ∧
(∀n. g n ≤ g (SUC n)) ⇒
(sup (IMAGE (λn. f n + g n) 𝕌(:num)) =
sup (IMAGE f 𝕌(:num)) + sup (IMAGE g 𝕌(:num)))
- sup_sum_mono
-
|- ∀f s.
FINITE s ∧ (∀i. i ∈ s ⇒ ∀n. 0 ≤ f i n) ∧
(∀i. i ∈ s ⇒ ∀n. f i n ≤ f i (SUC n)) ⇒
(sup (IMAGE (λn. SIGMA (λi. f i n) s) 𝕌(:num)) =
SIGMA (λi. sup (IMAGE (f i) 𝕌(:num))) s)
- sup_le_mono
-
|- ∀f z. (∀n. f n ≤ f (SUC n)) ∧ z < sup (IMAGE f 𝕌(:num)) ⇒ ∃n. z ≤ f n
- sup_cmul
-
|- ∀f c.
0 ≤ c ⇒
(sup (IMAGE (λn. Normal c * f n) 𝕌(:α)) = Normal c * sup (IMAGE f 𝕌(:α)))
- sup_lt
-
|- ∀P y. (∃x. P x ∧ y < x) ⇔ y < sup P
- sup_lt_epsilon
-
|- ∀P e.
0 < e ∧ (∃x. P x ∧ x ≠ NegInf) ∧ sup P ≠ PosInf ⇒ ∃x. P x ∧ sup P < x + e
- inf_le_imp
-
|- ∀p x. p x ⇒ inf p ≤ x
- le_inf
-
|- ∀p x. x ≤ inf p ⇔ ∀y. p y ⇒ x ≤ y
- inf_le
-
|- ∀p x. inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
- inf_eq
-
|- ∀p x. (inf p = x) ⇔ (∀y. p y ⇒ x ≤ y) ∧ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x
- inf_const
-
|- ∀x. inf (λy. y = x) = x
- inf_const_alt
-
|- ∀p z. (∃x. p x) ∧ (∀x. p x ⇒ (x = z)) ⇒ (inf p = z)
- inf_const_over_set
-
|- ∀s k. s ≠ ∅ ⇒ (inf (IMAGE (λx. k) s) = k)
- inf_suc
-
|- ∀f.
(∀m n. m ≤ n ⇒ f n ≤ f m) ⇒
(inf (IMAGE (λn. f (SUC n)) 𝕌(:num)) = inf (IMAGE f 𝕌(:num)))
- inf_seq
-
|- ∀f l.
mono_decreasing f ⇒
(f --> l ⇔ (inf (IMAGE (λn. Normal (f n)) 𝕌(:num)) = Normal l))
- inf_lt_infty
-
|- ∀p. NegInf < inf p ⇒ ∀x. p x ⇒ NegInf < x
- inf_min
-
|- ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ (inf p = z)
- inf_cminus
-
|- ∀f c.
Normal c − inf (IMAGE f 𝕌(:α)) = sup (IMAGE (λn. Normal c − f n) 𝕌(:α))
- ext_suminf_add
-
|- ∀f g.
(∀n. 0 ≤ f n ∧ 0 ≤ g n) ⇒ (suminf (λn. f n + g n) = suminf f + suminf g)
- ext_suminf_cmul
-
|- ∀f c. 0 ≤ c ∧ (∀n. 0 ≤ f n) ⇒ (suminf (λn. c * f n) = c * suminf f)
- ext_suminf_cmul_alt
-
|- ∀f c.
0 ≤ c ∧ ((∀n. f n ≠ NegInf) ∨ ∀n. f n ≠ PosInf) ⇒
(suminf (λn. Normal c * f n) = Normal c * suminf f)
- ext_suminf_lt_infty
-
|- ∀f. (∀n. 0 ≤ f n) ∧ suminf f ≠ PosInf ⇒ ∀n. f n < PosInf
- ext_suminf_suminf
-
|- ∀r.
(∀n. 0 ≤ r n) ∧ suminf (λn. Normal (r n)) ≠ PosInf ⇒
(suminf (λn. Normal (r n)) = Normal (suminf r))
- ext_suminf_mono
-
|- ∀f g. (∀n. g n ≠ NegInf ∧ g n ≤ f n) ⇒ suminf g ≤ suminf f
- ext_suminf_sub
-
|- ∀f g.
(∀n. 0 ≤ g n ∧ g n ≤ f n) ∧ suminf f ≠ PosInf ⇒
(suminf (λi. f i − g i) = suminf f − suminf g)
- ext_suminf_sum
-
|- ∀f n.
(∀n. 0 ≤ f n) ∧ (∀m. n ≤ m ⇒ (f m = 0)) ⇒ (suminf f = SIGMA f (count n))
- min_le
-
|- ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z
- min_le1
-
|- ∀x y. min x y ≤ x
- min_le2
-
|- ∀x y. min x y ≤ y
- le_min
-
|- ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y
- min_le2_imp
-
|- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2
- min_refl
-
|- ∀x. min x x = x
- min_comm
-
|- ∀x y. min x y = min y x
- min_infty
-
|- ∀x.
(min x PosInf = x) ∧ (min PosInf x = x) ∧ (min NegInf x = NegInf) ∧
(min x NegInf = NegInf)
- le_max
-
|- ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y
- le_max1
-
|- ∀x y. x ≤ max x y
- le_max2
-
|- ∀x y. y ≤ max x y
- max_le
-
|- ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z
- max_le2_imp
-
|- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2
- max_refl
-
|- ∀x. max x x = x
- max_comm
-
|- ∀x y. max x y = max y x
- max_infty
-
|- ∀x.
(max x PosInf = PosInf) ∧ (max PosInf x = PosInf) ∧ (max NegInf x = x) ∧
(max x NegInf = x)
- Q_not_infty
-
|- ∀x. x ∈ Q_set ⇒ ∃y. x = Normal y
- Q_COUNTABLE
-
|- countable Q_set
- NUM_IN_Q
-
|- ∀n. &n ∈ Q_set ∧ -&n ∈ Q_set
- Q_INFINITE
-
|- INFINITE Q_set
- OPP_IN_Q
-
|- ∀x. x ∈ Q_set ⇒ -x ∈ Q_set
- INV_IN_Q
-
|- ∀x. x ∈ Q_set ∧ x ≠ 0 ⇒ 1 / x ∈ Q_set
- CMUL_IN_Q
-
|- ∀z x. x ∈ Q_set ⇒ &z * x ∈ Q_set ∧ -&z * x ∈ Q_set
- ADD_IN_Q
-
|- ∀x y. x ∈ Q_set ∧ y ∈ Q_set ⇒ x + y ∈ Q_set
- SUB_IN_Q
-
|- ∀x y. x ∈ Q_set ∧ y ∈ Q_set ⇒ x − y ∈ Q_set
- MUL_IN_Q
-
|- ∀x y. x ∈ Q_set ∧ y ∈ Q_set ⇒ x * y ∈ Q_set
- DIV_IN_Q
-
|- ∀x y. x ∈ Q_set ∧ y ∈ Q_set ∧ y ≠ 0 ⇒ x / y ∈ Q_set
- rat_not_infty
-
|- ∀r. r ∈ Q_set ⇒ r ≠ NegInf ∧ r ≠ PosInf
- CEILING_LBOUND
-
|- ∀x. Normal x ≤ &ceiling (Normal x)
- CEILING_UBOUND
-
|- ∀x. 0 ≤ x ⇒ &ceiling (Normal x) < Normal x + 1
- Q_DENSE_IN_R_LEMMA
-
|- ∀x y. 0 ≤ x ∧ x < y ⇒ ∃r. r ∈ Q_set ∧ x < r ∧ r < y
- Q_DENSE_IN_R
-
|- ∀x y. x < y ⇒ ∃r. r ∈ Q_set ∧ x < r ∧ r < y
- COUNTABLE_ENUM_Q
-
|- ∀c. countable c ⇔ (c = ∅) ∨ ∃f. c = IMAGE f Q_set
- CROSS_COUNTABLE_UNIV
-
|- countable (𝕌(:num) × 𝕌(:num))
- CROSS_COUNTABLE_LEMMA1
-
|- ∀s. countable s ∧ FINITE s ∧ countable t ⇒ countable (s × t)
- CROSS_COUNTABLE_LEMMA2
-
|- ∀s. countable s ∧ countable t ∧ FINITE t ⇒ countable (s × t)
- CROSS_COUNTABLE
-
|- ∀s. countable s ∧ countable t ⇒ countable (s × t)
- COUNTABLE_RATIONAL_INTERVALS
-
|- countable rational_intervals