The Theory %real%
Parents
orders dyadic
Children
analysis
Constants
Is_ℝ_Rep
 DYADIC SET → BOOL
$<R
 ℝ → ℝ → BOOL
$≤R
 ℝ → ℝ → BOOL
$>R
 ℝ → ℝ → BOOL
$≥R
 ℝ → ℝ → BOOL
Sup
 ℝ SET → ℝ
1R
 ℝ
0R
 ℝ
$+R
 ℝ → ℝ → ℝ
~R
 ℝ → ℝ
$-R
 ℝ → ℝ → ℝ
ℕℝ
 ℕ → ℝ
AbsR
 ℝ → ℝ
$*R
 ℝ → ℝ → ℝ
$/R
 ℝ → ℝ → ℝ
$/N
 ℕ → ℕ → ℝ
$-1
 ℝ → ℝ
$^N
 ℝ → ℕ → ℝ
ℤℝ
 ℤ → ℝ
$^Z
 ℝ → ℤ → ℝ
Float
 ℕ → ℤ → ℤ → ℝ
MaxR
 ℝ LIST → ℝ
MinR
 ℝ LIST → ℝ
Aliases
<
 $<R : ℝ → ℝ → BOOL
≤
 $≤R : ℝ → ℝ → BOOL
>
 $>R : ℝ → ℝ → BOOL
≥
 $≥R : ℝ → ℝ → BOOL
+
 $+R : ℝ → ℝ → ℝ
~
 ~R : ℝ → ℝ
-
 $-R : ℝ → ℝ → ℝ
Abs
 AbsR : ℝ → ℝ
*
 $*R : ℝ → ℝ → ℝ
/
 $/R : ℝ → ℝ → ℝ
/
 $/N : ℕ → ℕ → ℝ
^
 $^N : ℝ → ℕ → ℝ
^
 $^Z : ℝ → ℤ → ℝ
Types
ℝ
Fixity
Left Infix 305:
-R
Left Infix 315:
/ /N /R
Right Infix 210:
<R >R ≤R ≥R
Right Infix 300:
+R
Right Infix 310:
*R
Right Infix 320:
^N ^Z
Postfix 320: -1
Definitions
Is_ℝ_Rep
 ⊢ ∀ a• Is_ℝ_Rep a ⇔ a ∈ Cuts (Universe, $dy_less)
ℝ
ℝ_def
 ⊢ ∃ f• TypeDefn Is_ℝ_Rep f
<R
 ⊢ ConstSpec
fill(λ <R'
fill• StrictLinearOrder (Universe, <R')
fill∧ UnboundedBelow (Universe, <R')
fill∧ UnboundedAbove (Universe, <R')
fill∧ Complete (Universe, <R')
fill∧ (∃ ι
fill• (∀ a b• <R' (ι a) (ι b) ⇔ a dy_less b)
fill∧ {x|∃ a• ι a = x}
fillDenseIn (Universe, <R')))
fill$<
≤R
 ⊢ ∀ x y• x ≤ y ⇔ x < y ∨ x = y
>R
 ⊢ ∀ x y• x > y ⇔ y < x
≥R
 ⊢ ∀ x y• x ≥ y ⇔ y ≤ x
Sup
 ⊢ ConstSpec
fill(λ Sup'
fill• ∀ A
fill• ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b)
fill⇒ (∀ x• x ∈ A ⇒ x ≤ Sup' A)
fill∧ (∀ b
fill• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup' A ≤ b))
fillSup
+R
0R
1R
 ⊢ ConstSpec
fill(λ (+R', 0R', 1R')
fill• (∀ x y z
fill• +R' (+R' x y) z = +R' x (+R' y z))
fill∧ (∀ x y• +R' x y = +R' y x)
fill∧ (∀ x• +R' x 0R' = x)
fill∧ (∀ x• ∃ y• +R' x y = 0R')
fill∧ (∀ x y z• y < z ⇒ +R' x y < +R' x z)
fill∧ 0R' < 1R')
fill($+, 0R, 1R)
~R
 ⊢ ConstSpec (λ ~R'• ∀ x• x + ~R' x = 0R) ~
-R
 ⊢ ∀ x y• x - y = x + ~ y
ℕℝ
 ⊢ 0. = 0R ∧ (∀ m• ℕℝ (m + 1) = ℕℝ m + 1R)
AbsR
 ⊢ ∀ x• Abs x = (if 0. ≤ x then x else ~ x)
*R
 ⊢ ConstSpec
fill(λ *R'
fill• (∀ x y z
fill• *R' (*R' x y) z = *R' x (*R' y z))
fill∧ (∀ x• *R' x 1. = x)
fill∧ (∀ x y z
fill• *R' x (y + z) = *R' x y + *R' x z)
fill∧ (∀ x y• *R' x y = *R' y x)
fill∧ (∀ x y• 0. < x ∧ 0. < y ⇒ 0. < *R' x y))
fill$*
/R
 ⊢ ConstSpec
fill(λ /R'
fill• (∀ y z• ¬ z = 0. ⇒ /R' (y * z) z = y)
fill∧ (∀ x y z
fill• ¬ z = 0. ⇒ /R' (x * y) z = x * /R' y z))
fill$/
/N
 ⊢ ∀ m n• m / n = ℕℝ m / ℕℝ n
-1
 ⊢ ∀ x• x -1 = 1. / x
^N
 ⊢ (∀ x• x ^ 0 = 1.) ∧ (∀ x m• x ^ (m + 1) = x * x ^ m)
ℤℝ
 ⊢ ConstSpec
fill(λ $"ℤℝ'"
fill• $"ℤℝ'" (ℕℤ 0) = 0.
fill∧ $"ℤℝ'" (ℕℤ 1) = 1.
fill∧ (∀ i j
fill• $"ℤℝ'" (i + j) = $"ℤℝ'" i + $"ℤℝ'" j))
fillℤℝ
^Z
 ⊢ ConstSpec
fill(λ ^Z'
fill• ∀ x m
fill• ^Z' x (ℕℤ m) = x ^ m
fill∧ ^Z' x (~ (ℕℤ (m + 1)))
fill= (x ^ (m + 1)) -1)
fill$^
Float
 ⊢ ∀ m p e• Float m p e = ℕℝ m * 10. ^ (e + ~ p)
MaxR
 ⊢ ConstSpec
fill(λ MaxR'
fill• (∀ x• MaxR' [x] = x)
fill∧ (∀ x y L
fill• MaxR' (Cons x (Cons y L))
fill= (if x < MaxR' (Cons y L)
fillthen MaxR' (Cons y L)
fillelse x)))
fillMaxR
MinR
 ⊢ ConstSpec
fill(λ MinR'
fill• (∀ x• MinR' [x] = x)
fill∧ (∀ x y L
fill• MinR' (Cons x (Cons y L))
fill= (if x > MinR' (Cons y L)
fillthen MinR' (Cons y L)
fillelse x)))
fillMinR
Theorems
dy_less_order_lemmas_thm
⊢ StrictLinearOrder (Universe, $dy_less)
fill∧ UnboundedBelow (Universe, $dy_less)
fill∧ UnboundedAbove (Universe, $dy_less)
fill∧ Universe DenseIn (Universe, $dy_less)
is_ℝ_rep_consistent_thm
⊢ ∃ a• Is_ℝ_Rep a
<R_consistent
⊢ Consistent
fill(λ <R'
fill• StrictLinearOrder (Universe, <R')
fill∧ UnboundedBelow (Universe, <R')
fill∧ UnboundedAbove (Universe, <R')
fill∧ Complete (Universe, <R')
fill∧ (∃ ι
fill• (∀ a b• <R' (ι a) (ι b) ⇔ a dy_less b)
fill∧ {x|∃ a• ι a = x}
fillDenseIn (Universe, <R')))
ℝ_unbounded_below_thm
⊢ ∀ x• ∃ y• y < x
ℝ_unbounded_above_thm
⊢ ∀ x• ∃ y• x < y
ℝ_less_irrefl_thm
⊢ ∀ x• ¬ x < x
ℝ_less_antisym_thm
⊢ ∀ x y• ¬ (x < y ∧ y < x)
ℝ_less_trans_thm
⊢ ∀ x y z• x < y ∧ y < z ⇒ x < z
ℝ_less_cases_thm
⊢ ∀ x y• x < y ∨ x = y ∨ y < x
ℝ_≤_cases_thm
⊢ ∀ x y• x ≤ y ∨ y ≤ x
ℝ_≤_less_cases_thm
⊢ ∀ x y• x ≤ y ∨ y < x
ℝ_eq_≤_thm
 ⊢ ∀ x y• x = y ⇔ x ≤ y ∧ y ≤ x
ℝ_≤_antisym_thm
⊢ ∀ x y• x ≤ y ∧ y ≤ x ⇒ x = y
ℝ_less_≤_trans_thm
⊢ ∀ x y z• x < y ∧ y ≤ z ⇒ x < z
ℝ_≤_less_trans_thm
⊢ ∀ x y z• x ≤ y ∧ y < z ⇒ x < z
ℝ_≤_refl_thm
 ⊢ ∀ x• x ≤ x
ℝ_≤_trans_thm
⊢ ∀ x y z• x ≤ y ∧ y ≤ z ⇒ x ≤ z
ℝ_≤_¬_less_thm
⊢ ∀ x y• x ≤ y ⇔ ¬ y < x
ℝ_¬_≤_less_thm
⊢ ∀ x y• ¬ x ≤ y ⇔ y < x
ℝ_less_¬_eq_thm
⊢ ∀ x y• x < y ⇒ ¬ x = y
ℝ_less_dense_thm
⊢ ∀ x y• x < y ⇒ (∃ z• x < z ∧ z < y)
ℝ_complete_thm
⊢ ∀ A
fill• ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b)
fill⇒ (∃ s
fill• (∀ x• x ∈ A ⇒ x ≤ s)
fill∧ (∀ b• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ s ≤ b))
Sup_consistent
⊢ Consistent
fill(λ Sup'
fill• ∀ A
fill• ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b)
fill⇒ (∀ x• x ∈ A ⇒ x ≤ Sup' A)
fill∧ (∀ b
fill• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup' A ≤ b))
ℝ_sup_thm
 ⊢ ∀ A a
fill• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a)
fill⇒ (∀ x• x ∈ A ⇒ x ≤ Sup A)
fill∧ (∀ b• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup A ≤ b)
ℝ_less_sup_thm
⊢ ∀ A
fill• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill⇒ (∀ x• x < Sup A ⇔ (∃ y• y ∈ A ∧ x < y))
ℝ_less_sup_bc_thm
⊢ ∀ A x
fill• ¬ A = {}
fill∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill∧ (∃ y• y ∈ A ∧ x < y)
fill⇒ x < Sup A
ℝ_≤_sup_thm
 ⊢ ∀ A a
fill• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill⇒ (∀ x
fill• x ≤ Sup A
fill⇔ (∀ y• (∀ z• z ∈ A ⇒ z ≤ y) ⇒ x ≤ y))
ℝ_≤_sup_bc_thm
⊢ ∀ A a x
fill• ¬ A = {}
fill∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill∧ (∀ y• (∀ z• z ∈ A ⇒ z ≤ y) ⇒ x ≤ y)
fill⇒ x ≤ Sup A
ℝ_∈_≤_sup_bc_thm
⊢ ∀ A x• x ∈ A ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ⇒ x ≤ Sup A
ℝ_⊆_sup_thm
 ⊢ ∀ A B
fill• ¬ A = {}
fill∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill∧ ¬ B = {}
fill∧ (∃ b• ∀ y• y ∈ B ⇒ y ≤ b)
fill∧ A ⊆ B
fill⇒ Sup A ≤ Sup B
ℝ_sup_≤_bc_thm
⊢ ∀ A a x
fill• ¬ A = {}
fill∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill∧ (∀ y• y ∈ A ⇒ y ≤ x)
fill⇒ Sup A ≤ x
ℝ_sup_less_bc_thm
⊢ ∀ A x z
fill• ¬ A = {}
fill∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a)
fill∧ (∀ y• y ∈ A ⇒ y ≤ x)
fill∧ x < z
fill⇒ Sup A < z
ℝ_sup_eq_bc_thm
⊢ ∀ A a s
fill• ¬ A = {}
fill∧ (∀ x• x ∈ A ⇒ x ≤ s)
fill∧ (∀ x• (∀ y• y ∈ A ⇒ y ≤ x) ⇒ s ≤ x)
fill⇒ Sup A = s
ℝ_eq_sup_bc_thm
⊢ ∀ A a s
fill• ¬ A = {}
fill∧ (∀ x• x ∈ A ⇒ x ≤ s)
fill∧ (∀ x• (∀ y• y ∈ A ⇒ y ≤ x) ⇒ s ≤ x)
fill⇒ s = Sup A
ℝ_less_sup_∈_thm
⊢ ∀ A a
fill• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a) ∧ ¬ Sup A ∈ A
fill⇒ (∀ x
fill• x < Sup A ⇒ (∃ y• x < y ∧ y < Sup A ∧ y ∈ A))
+R_consistent
0R_consistent
1R_consistent
⊢ Consistent
fill(λ (+R', 0R', 1R')
fill• (∀ x y z
fill• +R' (+R' x y) z = +R' x (+R' y z))
fill∧ (∀ x y• +R' x y = +R' y x)
fill∧ (∀ x• +R' x 0R' = x)
fill∧ (∀ x• ∃ y• +R' x y = 0R')
fill∧ (∀ x y z• y < z ⇒ +R' x y < +R' x z)
fill∧ 0R' < 1R')
~R_consistent
⊢ Consistent (λ ~R'• ∀ x• x + ~R' x = 0R)
ℝ_plus_assoc_thm
⊢ ∀ x y z• (x + y) + z = x + y + z
ℝ_plus_comm_thm
⊢ ∀ x y• x + y = y + x
ℝ_plus_unit_thm
⊢ ∀ x• x + 0R = x
ℝ_plus_mono_thm
⊢ ∀ x y z• y < z ⇒ x + y < x + z
ℝ_plus_assoc_thm1
⊢ ∀ x y z• x + y + z = (x + y) + z
ℝ_plus_mono_thm1
⊢ ∀ x y z• y < z ⇒ y + x < z + x
ℝ_plus_mono_thm2
⊢ ∀ x y s t• x < y ∧ s < t ⇒ x + s < y + t
ℝ_plus_0_thm
 ⊢ ∀ x• x + 0. = x ∧ 0. + x = x
ℝ_0_1_thm
 ⊢ 0R = 0. ∧ 1R = 1.
ℝ_plus_order_thm
⊢ ∀ x y z
fill• y + x = x + y
fill∧ (x + y) + z = x + y + z
fill∧ y + x + z = x + y + z
ℝ_plus_minus_thm
⊢ ∀ x• x + ~ x = 0. ∧ ~ x + x = 0.
ℝ_eq_thm
 ⊢ ∀ x y• x = y ⇔ x + ~ y = 0.
ℕℝ_plus_homomorphism_thm
⊢ ∀ m n• ℕℝ (m + n) = ℕℝ m + ℕℝ n
ℝ_minus_clauses
⊢ ∀ x y
fill• ~ (~ x) = x
fill∧ x + ~ x = 0.
fill∧ ~ x + x = 0.
fill∧ ~ (x + y) = ~ x + ~ y
fill∧ ~ 0. = 0.
ℝ_minus_eq_thm
⊢ ∀ x y• ~ x = ~ y ⇔ x = y
ℕℝ_0_less_thm
⊢ ∀ m• 0. < ℕℝ (m + 1)
ℕℝ_one_one_thm
⊢ ∀ m n• ℕℝ m = ℕℝ n ⇔ m = n
ℝ_plus_clauses
⊢ ∀ x y z
fill• (x + z = y + z ⇔ x = y)
fill∧ (z + x = y + z ⇔ x = y)
fill∧ (x + z = z + y ⇔ x = y)
fill∧ (z + x = z + y ⇔ x = y)
fill∧ (x + z = z ⇔ x = 0.)
fill∧ (z + x = z ⇔ x = 0.)
fill∧ (z = z + y ⇔ y = 0.)
fill∧ (z = y + z ⇔ y = 0.)
fill∧ x + 0. = x
fill∧ 0. + x = x
fill∧ ¬ 1. = 0.
fill∧ ¬ 0. = 1.
ℝ_less_less_0_thm
⊢ ∀ x y• x < y ⇔ x + ~ y < 0.
ℝ_less_clauses
⊢ ∀ x y z
fill• (x + z < y + z ⇔ x < y)
fill∧ (z + x < y + z ⇔ x < y)
fill∧ (x + z < z + y ⇔ x < y)
fill∧ (z + x < z + y ⇔ x < y)
fill∧ (x + z < z ⇔ x < 0.)
fill∧ (z + x < z ⇔ x < 0.)
fill∧ (x < z + x ⇔ 0. < z)
fill∧ (x < x + z ⇔ 0. < z)
fill∧ ¬ x < x
fill∧ 0. < 1.
fill∧ ¬ 1. < 0.
ℝ_less_0_less_thm
⊢ ∀ x y• x < y ⇔ 0. < y + ~ x
ℝ_≤_clauses
 ⊢ ∀ x y z
fill• (x + z ≤ y + z ⇔ x ≤ y)
fill∧ (z + x ≤ y + z ⇔ x ≤ y)
fill∧ (x + z ≤ z + y ⇔ x ≤ y)
fill∧ (z + x ≤ z + y ⇔ x ≤ y)
fill∧ (x + z ≤ z ⇔ x ≤ 0.)
fill∧ (z + x ≤ z ⇔ x ≤ 0.)
fill∧ (x ≤ z + x ⇔ 0. ≤ z)
fill∧ (x ≤ x + z ⇔ 0. ≤ z)
fill∧ x ≤ x
fill∧ 0. ≤ 1.
fill∧ ¬ 1. ≤ 0.
ℝ_≤_≤_0_thm
 ⊢ ∀ x y• x ≤ y ⇔ x + ~ y ≤ 0.
ℝ_≤_0_≤_thm
 ⊢ ∀ x y• x ≤ y ⇔ 0. ≤ y + ~ x
ℕℝ_less_thm
 ⊢ ∀ m n• ℕℝ m < ℕℝ n ⇔ m < n
ℝ_less_strong_dense_thm
⊢ ∀ x y• x < y ⇒ (∃ d• 0. < d ∧ x + d < y)
ℕℝ_≤_thm
 ⊢ ∀ m n• ℕℝ m ≤ ℕℝ n ⇔ m ≤ n
ℝ_sup_plus_thm
⊢ ∀ A a x
fill• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a)
fill⇒ Sup A + x = Sup {t|∃ a• a ∈ A ∧ t < a + x}
ℝ_sup_plus_sup_thm
⊢ ∀ A a B b
fill• ¬ A = {}
fill∧ (∀ x• x ∈ A ⇒ x ≤ a)
fill∧ ¬ B = {}
fill∧ (∀ y• y ∈ B ⇒ y ≤ b)
fill⇒ Sup A + Sup B
fill= Sup {t|∃ a b• a ∈ A ∧ b ∈ B ∧ t < a + b}
ℝ_delta_induction_thm
⊢ ∀ x p
fill• (∃ d
fill• 0. < d
fill∧ (∃ e
fill• d < e ∧ (∀ t• x < t ∧ t < x + e ⇒ p t))
fill∧ (∀ s• x < s ∧ p s ⇒ p (s + d)))
fill⇒ (∀ y• x < y ⇒ p y)
ℝ_ord_pres_strict_thm
⊢ ∀ f
fill• (∀ x y• x < y ⇒ f x < f y)
fill⇒ (∀ x y• f x < f y ⇒ x < y)
ℝ_add_hom_0_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• f 0. = 0.)
ℝ_add_hom_minus_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• f (~ x) = ~ (f x))
ℝ_add_hom_extension_thm
⊢ ∀ f
fill• (∀ x y• 0. ≤ x ∧ 0. ≤ y ⇒ f (x + y) = f x + f y)
fill∧ (∀ x• 0. ≤ x ⇒ f (~ x) = ~ (f x))
fill⇒ (∀ x y• f (x + y) = f x + f y)
ℝ_monoid_delta_dense_thm
⊢ ∀ G d
fill• 0. ∈ G
fill∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G)
fill∧ d ∈ G
fill∧ 0. < d
fill⇒ (∀ x
fill• 0. < x ⇒ (∃ g• g ∈ G ∧ g ≤ x ∧ x < g + d))
ℝ_monoid_dense_thm
⊢ ∀ G
fill• 0. ∈ G
fill∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G)
fill∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x))
fill⇒ (∀ x y
fill• 0. < x ∧ x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y))
ℝ_subgroup_dense_thm
⊢ ∀ G
fill• 0. ∈ G
fill∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G)
fill∧ (∀ g• g ∈ G ⇒ ~ g ∈ G)
fill∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x))
fill⇒ (∀ x y• x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y))
ℝ_semigroup_dense_thm
⊢ ∀ G
fill• (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G)
fill∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x))
fill⇒ (∀ x y
fill• 0. < x ∧ x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y))
ℝ_add_hom_image_group_thm
⊢ ∀ f I
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ I = {b|∃ a• b = f a}
fill⇒ 0. ∈ I
fill∧ (∀ g h• g ∈ I ∧ h ∈ I ⇒ g + h ∈ I)
fill∧ (∀ g• g ∈ I ⇒ ~ g ∈ I)
ℝ_add_hom_kernel_group_thm
⊢ ∀ f K
fill• (∀ x y• f (x + y) = f x + f y) ∧ K = {a|f a = 0.}
fill⇒ 0. ∈ K
fill∧ (∀ g h• g ∈ K ∧ h ∈ K ⇒ g + h ∈ K)
fill∧ (∀ g• g ∈ K ⇒ ~ g ∈ K)
ℝ_opah_thm
 ⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ (∀ x y• x < y ⇒ f x < f y)
ℝ_opah_strict_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ (∀ x y• f x < f y ⇒ x < y)
ℝ_opah_one_one_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ OneOne f
ℝ_opah_dense_image_thm
⊢ ∀ f e
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill∧ 0. < e
fill⇒ (∃ d• 0. < d ∧ f d < e)
ℝ_opah_onto_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ Onto f
ℝ_opah_inverse_add_hom_thm
⊢ ∀ f g
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill∧ (∀ x• g (f x) = x)
fill∧ (∀ x• f (g x) = x)
fill⇒ (∀ x y• g (x + y) = g x + g y)
fill∧ (∀ x• 0. < x ⇒ 0. < g x)
ℝ_opah_inverse_thm
⊢ ∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ (∃ g
fill• (∀ x• g (f x) = x)
fill∧ (∀ x• f (g x) = x)
fill∧ (∀ x y• g (x + y) = g x + g y)
fill∧ (∀ x• 0. < x ⇒ 0. < g x))
ℝ_copah_id_thm
⊢ ∃ ι
fill• (∀ x• ι x = x)
fill∧ (∀ x y• ι (x + y) = ι x + ι y)
fill∧ (∀ x• 0. < x ⇒ 0. < ι x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• ι (f x) = f (ι x)))
ℝ_copah_double_thm
⊢ ∃ α
fill• (∀ x• α x = x + x)
fill∧ (∀ x y• α (x + y) = α x + α y)
fill∧ (∀ x• 0. < x ⇒ 0. < α x)
fill∧ (∀ x• 0. < x ⇒ x < α x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• α (f x) = f (α x)))
ℝ_copah_halve_thm
⊢ ∃ β
fill• (∀ x• β x + β x = x)
fill∧ (∀ x y• β (x + y) = β x + β y)
fill∧ (∀ x• 0. < x ⇒ 0. < β x)
fill∧ (∀ x• 0. < x ⇒ β x < x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• β (f x) = f (β x)))
ℝ_copah_comp_thm
⊢ ∀ α β
fill• (∀ x y• α (x + y) = α x + α y)
fill∧ (∀ x• 0. < x ⇒ 0. < α x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• α (f x) = f (α x)))
fill∧ (∀ x y• β (x + y) = β x + β y)
fill∧ (∀ x• 0. < x ⇒ 0. < β x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• β (f x) = f (β x)))
fill⇒ (∃ γ
fill• (∀ x• γ x = α (β x))
fill∧ (∀ x• 0. < x ⇒ 0. < γ x)
fill∧ (∀ x y• γ (x + y) = γ x + γ y)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• γ (f x) = f (γ x))))
ℝ_copah_sum_thm
⊢ ∀ α β
fill• (∀ x y• α (x + y) = α x + α y)
fill∧ (∀ x• 0. < x ⇒ 0. < α x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• α (f x) = f (α x)))
fill∧ (∀ x y• β (x + y) = β x + β y)
fill∧ (∀ x• 0. < x ⇒ 0. < β x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• β (f x) = f (β x)))
fill⇒ (∃ γ
fill• (∀ x• γ x = α x + β x)
fill∧ (∀ x• 0. < x ⇒ 0. < γ x)
fill∧ (∀ x y• γ (x + y) = γ x + γ y)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• γ (f x) = f (γ x))))
ℝ_halve_closed_dense_thm
⊢ ∀ A e
fill• 0. < e
fill∧ e ∈ A
fill∧ (∀ y• y ∈ A ⇒ (∃ z• z ∈ A ∧ z + z = y))
fill⇒ (∀ d• 0. < d ⇒ (∃ a• a ∈ A ∧ 0. < a ∧ a < d))
ℝ_copah_dense_thm
⊢ ∀ d x y
fill• 0. < d ∧ 0. < x ∧ x < y
fill⇒ (∃ γ
fill• (∀ x y• γ (x + y) = γ x + γ y)
fill∧ (∀ x• 0. < x ⇒ 0. < γ x)
fill∧ (∀ f
fill• (∀ x y• f (x + y) = f x + f y)
fill⇒ (∀ x• γ (f x) = f (γ x)))
fill∧ x < γ d
fill∧ γ d < y)
ℝ_opah_extension_thm1
⊢ ∀ f
fill• (∀ x y• 0. < x ∧ 0. < y ⇒ f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ (∃ φ
fill• φ 0. = 0.
fill∧ (∀ x• 0. < x ⇒ φ x = f x)
fill∧ (∀ x y
fill• 0. ≤ x ∧ 0. ≤ y ⇒ φ (x + y) = φ x + φ y))
ℝ_opah_extension_thm2
⊢ ∀ f
fill• f 0. = 0.
fill∧ (∀ x y
fill• 0. ≤ x ∧ 0. ≤ y ⇒ f (x + y) = f x + f y)
fill⇒ (∃ ψ
fill• (∀ x• 0. ≤ x ⇒ ψ x = f x)
fill∧ (∀ x y• ψ (x + y) = ψ x + ψ y))
ℝ_opah_extension_thm
⊢ ∀ f
fill• (∀ x y• 0. < x ∧ 0. < y ⇒ f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill⇒ (∃ φ
fill• (∀ x• 0. < x ⇒ φ x = f x)
fill∧ (∀ x y• φ (x + y) = φ x + φ y)
fill∧ (∀ x• 0. < x ⇒ 0. < φ x))
ℝ_opah_order_thm
⊢ ∀ f g d
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill∧ (∀ x y• g (x + y) = g x + g y)
fill∧ (∀ x• 0. < x ⇒ 0. < g x)
fill∧ 0. < d
fill∧ f d < g d
fill⇒ (∀ x• 0. < x ⇒ f x < g x)
ℝ_opah_eq_thm
⊢ ∀ f g d
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill∧ (∀ x y• g (x + y) = g x + g y)
fill∧ (∀ x• 0. < x ⇒ 0. < g x)
fill∧ 0. < d
fill∧ f d = g d
fill⇒ f = g
ℝ_opah_complete_thm
⊢ ∀ d e
fill• 0. < d ∧ 0. < e
fill⇒ (∃ f
fill• (∀ x y• f (x + y) = f x + f y)
fill∧ (∀ x• 0. < x ⇒ 0. < f x)
fill∧ f d = e)
*R_consistent
⊢ Consistent
fill(λ *R'
fill• (∀ x y z
fill• *R' (*R' x y) z = *R' x (*R' y z))
fill∧ (∀ x• *R' x 1. = x)
fill∧ (∀ x y z
fill• *R' x (y + z) = *R' x y + *R' x z)
fill∧ (∀ x y• *R' x y = *R' y x)
fill∧ (∀ x y• 0. < x ∧ 0. < y ⇒ 0. < *R' x y))
ℝ_times_assoc_thm
⊢ ∀ x y z• (x * y) * z = x * y * z
ℝ_times_comm_thm
⊢ ∀ x y• x * y = y * x
ℝ_times_unit_thm
⊢ ∀ x• x * 1. = x
ℝ_0_less_0_less_times_thm
⊢ ∀ x y• 0. < x ∧ 0. < y ⇒ 0. < x * y
ℝ_times_assoc_thm1
⊢ ∀ x y z• x * y * z = (x * y) * z
ℝ_times_plus_distrib_thm
⊢ ∀ x y z
fill• x * (y + z) = x * y + x * z
fill∧ (x + y) * z = x * z + y * z
ℝ_times_order_thm
⊢ ∀ x y z
fill• y * x = x * y
fill∧ (x * y) * z = x * y * z
fill∧ y * x * z = x * y * z
ℝ_times_0_thm
⊢ ∀ x• x * 0. = 0. ∧ 0. * x = 0.
ℝ_times_1_thm
⊢ ∀ x• x * 1. = x ∧ 1. * x = x
ℕℝ_times_homomorphism_thm
⊢ ∀ m n• ℕℝ (m * n) = ℕℝ m * ℕℝ n
ℝ_times_minus_thm
⊢ ∀ x y
fill• ~ x * y = ~ (x * y)
fill∧ x * ~ y = ~ (x * y)
fill∧ ~ x * ~ y = x * y
/R_consistent
⊢ Consistent
fill(λ /R'
fill• (∀ y z• ¬ z = 0. ⇒ /R' (y * z) z = y)
fill∧ (∀ x y z
fill• ¬ z = 0. ⇒ /R' (x * y) z = x * /R' y z))
ℝ_over_times_recip_thm
⊢ ∀ z• ¬ z = 0. ⇒ (∀ x• x / z = x * z -1)
ℝ_times_recip_thm
⊢ ∀ z• ¬ z = 0. ⇒ z * z -1 = 1.
ℝ_eq_recip_thm
⊢ ∀ z• ¬ z = 0. ⇒ (∀ y• y = z ⇔ y * z -1 = 1.)
ℝ_times_cancel_thm
⊢ ∀ x y z• ¬ z = 0. ⇒ (x * z = y * z ⇔ x = y)
ℝ_times_eq_0_thm
⊢ ∀ x y• x * y = 0. ⇔ x = 0. ∨ y = 0.
ℝ_times_clauses
⊢ ∀ x
fill• 0. * x = 0. ∧ x * 0. = 0. ∧ x * 1. = x ∧ 1. * x = x
ℝ_times_mono_⇔_thm
⊢ ∀ x• 0. < x ⇒ (∀ y z• y < z ⇔ x * y < x * z)
ℝ_times_mono_thm
⊢ ∀ x y z• 0. < x ∧ y < z ⇒ x * y < x * z
ℝ_0_≤_0_≤_times_thm
⊢ ∀ x y• 0. ≤ x ∧ 0. ≤ y ⇒ 0. ≤ x * y
ℝ_¬_recip_0_thm
⊢ ∀ z• ¬ z = 0. ⇒ ¬ z -1 = 0.
ℝ_recip_clauses
⊢ (1. -1 = 1.
fill∧ (∀ w
fill• ¬ w = 0.
fill⇒ w -1 -1 = w
fill∧ w * w -1 = 1.
fill∧ w -1 * w = 1.))
fill∧ (∀ w z
fill• ¬ w = 0. ∧ ¬ z = 0.
fill⇒ (w * z) -1 = w -1 * z -1)
ℝ_cross_mult_eq_thm
⊢ ∀ w z
fill• ¬ w = 0. ∧ ¬ z = 0.
fill⇒ (∀ x y• x / w = y / z ⇔ x * z = w * y)
ℝ_less_¬_eq_0_thm
⊢ ∀ z• 0. < z ⇒ ¬ z = 0.
ℝ_0_less_0_less_recip_thm
⊢ ∀ z• 0. < z ⇒ 0. < z -1
ℝ_cross_mult_less_thm
⊢ ∀ w z
fill• 0. < w ∧ 0. < z
fill⇒ (∀ x y• x / w < y / z ⇔ x * z < w * y)
ℝ_over_cancel_eq_thm
⊢ ∀ w z
fill• ¬ w = 0. ∧ ¬ z = 0.
fill⇒ (∀ x• (x * z) / (w * z) = x / w)
ℝ_over_plus_over_thm
⊢ ∀ x y u v
fill• ¬ u = 0. ∧ ¬ v = 0.
fill⇒ x / u + y / v = (x * v + y * u) / (u * v)
ℝ_0_over_thm
 ⊢ ∀ z• ¬ z = 0. ⇒ 0. / z = 0.
ℝ_over_1_thm
 ⊢ ∀ x• x / 1. = x
ℕℝ_plus_homomorphism_thm1
⊢ ∀ m n• ℕℝ m + ℕℝ n = ℕℝ (m + n)
ℕℝ_times_homomorphism_thm1
⊢ ∀ m n• ℕℝ m * ℕℝ n = ℕℝ (m * n)
ℝ_frac_cross_mult_eq_thm
⊢ ∀ m n i j
fill• i / (m + 1) = j / (n + 1)
fill⇔ i * (n + 1) = j * (m + 1)
ℝ_frac_cancel_eq_thm
⊢ ∀ i m n
fill• (i * (n + 1)) / ((m + 1) * (n + 1)) = i / (m + 1)
ℝ_frac_0_thm
 ⊢ ∀ m• 0 / (m + 1) = 0.
ℝ_frac_ℕ_thm
 ⊢ ∀ i• i / 1 = ℕℝ i
ℝ_frac_plus_frac_thm
⊢ ∀ i j k m n
fill• i / (m + 1) + j / (n + 1)
fill= (i * (n + 1) + j * (m + 1))
fill/ ((m + 1) * (n + 1))
ℝ_frac_minus_frac_thm
⊢ ∀ i j k m n
fill• j * (m + 1) ≤ i * (n + 1)
fill⇒ i / (m + 1) + ~ (j / (n + 1))
fill= (i * (n + 1) - j * (m + 1))
fill/ ((m + 1) * (n + 1))
ℝ_frac_minus_frac_thm1
⊢ ∀ i j m n
fill• i * (n + 1) ≤ j * (m + 1)
fill⇒ i / (m + 1) + ~ (j / (n + 1))
fill= ~
fill((j * (m + 1) - i * (n + 1))
fill/ ((m + 1) * (n + 1)))
ℝ_over_times_over_thm
⊢ ∀ x y u v
fill• ¬ u = 0. ∧ ¬ v = 0.
fill⇒ x / u * y / v = (x * y) / (u * v)
ℝ_frac_times_frac_thm
⊢ ∀ i j m n
fill• i / (m + 1) * j / (n + 1)
fill= (i * j) / ((m + 1) * (n + 1))
ℝ_over_recip_thm
⊢ ∀ u v• ¬ u = 0. ∧ ¬ v = 0. ⇒ (u / v) -1 = v / u
ℝ_frac_recip_thm
⊢ ∀ m n• ((m + 1) / (n + 1)) -1 = (n + 1) / (m + 1)
ℝ_minus_recip_thm
⊢ ∀ z• ¬ z = 0. ⇒ ~ z -1 = ~ (z -1)
ℝ_over_eq_0_thm
⊢ ∀ u v• ¬ u = 0. ∧ ¬ v = 0. ⇒ ¬ u / v = 0.
ℝ_over_over_over_thm
⊢ ∀ x y u v
fill• ¬ u = 0. ∧ ¬ v = 0. ∧ ¬ y = 0.
fill⇒ x / u / (y / v) = (x * v) / (u * y)
ℝ_frac_less_frac_thm
⊢ ∀ i j m n
fill• i / (m + 1) < j / (n + 1)
fill⇔ i * (n + 1) < j * (m + 1)
ℝ_minus_frac_less_frac_thm
⊢ ∀ i j m n• ~ (i / (m + 1)) < j / (n + 1) ⇔ 0 < i + j
ℝ_frac_less_minus_frac_thm
⊢ ∀ i j m n• ¬ i / (m + 1) < ~ (j / (n + 1))
ℝ_0_≤_frac_thm
⊢ ∀ i m• 0. ≤ i / (m + 1)
ℝ_abs_frac_thm
⊢ ∀ i m• Abs (i / (m + 1)) = i / (m + 1)
ℝ_abs_minus_thm
⊢ ∀ x• Abs (~ x) = Abs x
MaxR_consistent
⊢ Consistent
fill(λ MaxR'
fill• (∀ x• MaxR' [x] = x)
fill∧ (∀ x y L
fill• MaxR' (Cons x (Cons y L))
fill= (if x < MaxR' (Cons y L)
fillthen MaxR' (Cons y L)
fillelse x)))
MinR_consistent
⊢ Consistent
fill(λ MinR'
fill• (∀ x• MinR' [x] = x)
fill∧ (∀ x y L
fill• MinR' (Cons x (Cons y L))
fill= (if x > MinR' (Cons y L)
fillthen MinR' (Cons y L)
fillelse x)))
ℝ_max_cons_thm
⊢ ∀ x L
fill• MaxR (Cons x L)
fill= (if L = []
fillthen x
fillelse if x < MaxR L
fillthen MaxR L
fillelse x)
ℝ_max_conv_thm
⊢ ∀ x y L
fill• MaxR (Cons x (Cons y L))
fill= (if x < y
fillthen MaxR (Cons y L)
fillelse MaxR (Cons x L))
ℝ_min_cons_thm
⊢ ∀ x L
fill• MinR (Cons x L)
fill= (if L = []
fillthen x
fillelse if MinR L < x
fillthen MinR L
fillelse x)
ℝ_min_conv_thm
⊢ ∀ x y L
fill• MinR (Cons x (Cons y L))
fill= (if x < y
fillthen MinR (Cons x L)
fillelse MinR (Cons y L))
^Z_consistent
⊢ Consistent
fill(λ ^Z'
fill• ∀ x m
fill• ^Z' x (ℕℤ m) = x ^ m
fill∧ ^Z' x (~ (ℕℤ (m + 1)))
fill= (x ^ (m + 1)) -1)
ℤℝ_consistent
⊢ Consistent
fill(λ $"ℤℝ'"
fill• $"ℤℝ'" (ℕℤ 0) = 0.
fill∧ $"ℤℝ'" (ℕℤ 1) = 1.
fill∧ (∀ i j
fill• $"ℤℝ'" (i + j) = $"ℤℝ'" i + $"ℤℝ'" j))
ℤℝ_plus_homomorphism_thm
⊢ ∀ i j• ℤℝ (i + j) = ℤℝ i + ℤℝ j
ℤℝ_minus_thm
 ⊢ ∀ i• ℤℝ (~ i) = ~ (ℤℝ i)
ℤℝ_ℕℤ_thm
 ⊢ ∀ m• ℤℝ (ℕℤ m) = ℕℝ m ∧ ℤℝ (~ (ℕℤ m)) = ~ (ℕℝ m)
ℤℝ_times_homomorphism_thm
⊢ ∀ i j• ℤℝ (i * j) = ℤℝ i * ℤℝ j

up quick index

privacy policy

Created:

V