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 (λ <R' • StrictLinearOrder (Universe, <R') ∧ UnboundedBelow (Universe, <R') ∧ UnboundedAbove (Universe, <R') ∧ Complete (Universe, <R') ∧ (∃ ι • (∀ a b• <R' (ι a) (ι b) ⇔ a dy_less b) ∧ {x|∃ a• ι a = x} DenseIn (Universe, <R'))) $< |
≤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 (λ Sup' • ∀ A • ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b) ⇒ (∀ x• x ∈ A ⇒ x ≤ Sup' A) ∧ (∀ b • (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup' A ≤ b)) Sup |
+R
0R
1R
|
⊢ ConstSpec (λ (+R', 0R', 1R') • (∀ x y z • +R' (+R' x y) z = +R' x (+R' y z)) ∧ (∀ x y• +R' x y = +R' y x) ∧ (∀ x• +R' x 0R' = x) ∧ (∀ x• ∃ y• +R' x y = 0R') ∧ (∀ x y z• y < z ⇒ +R' x y < +R' x z) ∧ 0R' < 1R') ($+, 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 (λ *R' • (∀ x y z • *R' (*R' x y) z = *R' x (*R' y z)) ∧ (∀ x• *R' x 1. = x) ∧ (∀ x y z • *R' x (y + z) = *R' x y + *R' x z) ∧ (∀ x y• *R' x y = *R' y x) ∧ (∀ x y• 0. < x ∧ 0. < y ⇒ 0. < *R' x y)) $* |
/R
|
⊢ ConstSpec (λ /R' • (∀ y z• ¬ z = 0. ⇒ /R' (y * z) z = y) ∧ (∀ x y z • ¬ z = 0. ⇒ /R' (x * y) z = x * /R' y z)) $/ |
/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 (λ $"ℤℝ'" • $"ℤℝ'" (ℕℤ 0) = 0. ∧ $"ℤℝ'" (ℕℤ 1) = 1. ∧ (∀ i j • $"ℤℝ'" (i + j) = $"ℤℝ'" i + $"ℤℝ'" j)) ℤℝ |
^Z
|
⊢ ConstSpec (λ ^Z' • ∀ x m • ^Z' x (ℕℤ m) = x ^ m ∧ ^Z' x (~ (ℕℤ (m + 1))) = (x ^ (m + 1)) -1) $^ |
Float
|
⊢ ∀ m p e• Float m p e = ℕℝ m * 10. ^ (e + ~ p) |
MaxR
|
⊢ ConstSpec (λ MaxR' • (∀ x• MaxR' [x] = x) ∧ (∀ x y L • MaxR' (Cons x (Cons y L)) = (if x < MaxR' (Cons y L) then MaxR' (Cons y L) else x))) MaxR |
MinR
|
⊢ ConstSpec (λ MinR' • (∀ x• MinR' [x] = x) ∧ (∀ x y L • MinR' (Cons x (Cons y L)) = (if x > MinR' (Cons y L) then MinR' (Cons y L) else x))) MinR |
Theorems |
dy_less_order_lemmas_thm
|
⊢ StrictLinearOrder (Universe, $dy_less)
∧ UnboundedBelow (Universe, $dy_less) ∧ UnboundedAbove (Universe, $dy_less) ∧ Universe DenseIn (Universe, $dy_less) |
is_ℝ_rep_consistent_thm
|
⊢ ∃ a• Is_ℝ_Rep a |
<R_consistent
|
⊢ Consistent
(λ <R' • StrictLinearOrder (Universe, <R') ∧ UnboundedBelow (Universe, <R') ∧ UnboundedAbove (Universe, <R') ∧ Complete (Universe, <R') ∧ (∃ ι • (∀ a b• <R' (ι a) (ι b) ⇔ a dy_less b) ∧ {x|∃ a• ι a = x} DenseIn (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
• ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b) ⇒ (∃ s • (∀ x• x ∈ A ⇒ x ≤ s) ∧ (∀ b• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ s ≤ b)) |
Sup_consistent
|
⊢ Consistent
(λ Sup' • ∀ A • ¬ A = {} ∧ (∃ b• ∀ x• x ∈ A ⇒ x ≤ b) ⇒ (∀ x• x ∈ A ⇒ x ≤ Sup' A) ∧ (∀ b • (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup' A ≤ b)) |
ℝ_sup_thm
|
⊢ ∀ A a • ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a) ⇒ (∀ x• x ∈ A ⇒ x ≤ Sup A) ∧ (∀ b• (∀ x• x ∈ A ⇒ x ≤ b) ⇒ Sup A ≤ b) |
ℝ_less_sup_thm
|
⊢ ∀ A
• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ⇒ (∀ x• x < Sup A ⇔ (∃ y• y ∈ A ∧ x < y)) |
ℝ_less_sup_bc_thm
|
⊢ ∀ A x
• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ∧ (∃ y• y ∈ A ∧ x < y) ⇒ x < Sup A |
ℝ_≤_sup_thm
|
⊢ ∀ A a • ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ⇒ (∀ x • x ≤ Sup A ⇔ (∀ y• (∀ z• z ∈ A ⇒ z ≤ y) ⇒ x ≤ y)) |
ℝ_≤_sup_bc_thm
|
⊢ ∀ A a x
• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ∧ (∀ y• (∀ z• z ∈ A ⇒ z ≤ y) ⇒ x ≤ y) ⇒ x ≤ Sup A |
ℝ_∈_≤_sup_bc_thm
|
⊢ ∀ A x• x ∈ A ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ⇒ x ≤ Sup A |
ℝ_⊆_sup_thm
|
⊢ ∀ A B • ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ∧ ¬ B = {} ∧ (∃ b• ∀ y• y ∈ B ⇒ y ≤ b) ∧ A ⊆ B ⇒ Sup A ≤ Sup B |
ℝ_sup_≤_bc_thm
|
⊢ ∀ A a x
• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ∧ (∀ y• y ∈ A ⇒ y ≤ x) ⇒ Sup A ≤ x |
ℝ_sup_less_bc_thm
|
⊢ ∀ A x z
• ¬ A = {} ∧ (∃ a• ∀ x• x ∈ A ⇒ x ≤ a) ∧ (∀ y• y ∈ A ⇒ y ≤ x) ∧ x < z ⇒ Sup A < z |
ℝ_sup_eq_bc_thm
|
⊢ ∀ A a s
• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ s) ∧ (∀ x• (∀ y• y ∈ A ⇒ y ≤ x) ⇒ s ≤ x) ⇒ Sup A = s |
ℝ_eq_sup_bc_thm
|
⊢ ∀ A a s
• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ s) ∧ (∀ x• (∀ y• y ∈ A ⇒ y ≤ x) ⇒ s ≤ x) ⇒ s = Sup A |
ℝ_less_sup_∈_thm
|
⊢ ∀ A a
• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a) ∧ ¬ Sup A ∈ A ⇒ (∀ x • x < Sup A ⇒ (∃ y• x < y ∧ y < Sup A ∧ y ∈ A)) |
+R_consistent
0R_consistent
1R_consistent
|
⊢ Consistent
(λ (+R', 0R', 1R') • (∀ x y z • +R' (+R' x y) z = +R' x (+R' y z)) ∧ (∀ x y• +R' x y = +R' y x) ∧ (∀ x• +R' x 0R' = x) ∧ (∀ x• ∃ y• +R' x y = 0R') ∧ (∀ x y z• y < z ⇒ +R' x y < +R' x z) ∧ 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
• y + x = x + y ∧ (x + y) + z = x + y + z ∧ 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
• ~ (~ x) = x ∧ x + ~ x = 0. ∧ ~ x + x = 0. ∧ ~ (x + y) = ~ x + ~ y ∧ ~ 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
• (x + z = y + z ⇔ x = y) ∧ (z + x = y + z ⇔ x = y) ∧ (x + z = z + y ⇔ x = y) ∧ (z + x = z + y ⇔ x = y) ∧ (x + z = z ⇔ x = 0.) ∧ (z + x = z ⇔ x = 0.) ∧ (z = z + y ⇔ y = 0.) ∧ (z = y + z ⇔ y = 0.) ∧ x + 0. = x ∧ 0. + x = x ∧ ¬ 1. = 0. ∧ ¬ 0. = 1. |
ℝ_less_less_0_thm
|
⊢ ∀ x y• x < y ⇔ x + ~ y < 0. |
ℝ_less_clauses
|
⊢ ∀ x y z
• (x + z < y + z ⇔ x < y) ∧ (z + x < y + z ⇔ x < y) ∧ (x + z < z + y ⇔ x < y) ∧ (z + x < z + y ⇔ x < y) ∧ (x + z < z ⇔ x < 0.) ∧ (z + x < z ⇔ x < 0.) ∧ (x < z + x ⇔ 0. < z) ∧ (x < x + z ⇔ 0. < z) ∧ ¬ x < x ∧ 0. < 1. ∧ ¬ 1. < 0. |
ℝ_less_0_less_thm
|
⊢ ∀ x y• x < y ⇔ 0. < y + ~ x |
ℝ_≤_clauses
|
⊢ ∀ x y z • (x + z ≤ y + z ⇔ x ≤ y) ∧ (z + x ≤ y + z ⇔ x ≤ y) ∧ (x + z ≤ z + y ⇔ x ≤ y) ∧ (z + x ≤ z + y ⇔ x ≤ y) ∧ (x + z ≤ z ⇔ x ≤ 0.) ∧ (z + x ≤ z ⇔ x ≤ 0.) ∧ (x ≤ z + x ⇔ 0. ≤ z) ∧ (x ≤ x + z ⇔ 0. ≤ z) ∧ x ≤ x ∧ 0. ≤ 1. ∧ ¬ 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
• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a) ⇒ Sup A + x = Sup {t|∃ a• a ∈ A ∧ t < a + x} |
ℝ_sup_plus_sup_thm
|
⊢ ∀ A a B b
• ¬ A = {} ∧ (∀ x• x ∈ A ⇒ x ≤ a) ∧ ¬ B = {} ∧ (∀ y• y ∈ B ⇒ y ≤ b) ⇒ Sup A + Sup B = Sup {t|∃ a b• a ∈ A ∧ b ∈ B ∧ t < a + b} |
ℝ_delta_induction_thm
|
⊢ ∀ x p
• (∃ d • 0. < d ∧ (∃ e • d < e ∧ (∀ t• x < t ∧ t < x + e ⇒ p t)) ∧ (∀ s• x < s ∧ p s ⇒ p (s + d))) ⇒ (∀ y• x < y ⇒ p y) |
ℝ_ord_pres_strict_thm
|
⊢ ∀ f
• (∀ x y• x < y ⇒ f x < f y) ⇒ (∀ x y• f x < f y ⇒ x < y) |
ℝ_add_hom_0_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• f 0. = 0.) |
ℝ_add_hom_minus_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• f (~ x) = ~ (f x)) |
ℝ_add_hom_extension_thm
|
⊢ ∀ f
• (∀ x y• 0. ≤ x ∧ 0. ≤ y ⇒ f (x + y) = f x + f y) ∧ (∀ x• 0. ≤ x ⇒ f (~ x) = ~ (f x)) ⇒ (∀ x y• f (x + y) = f x + f y) |
ℝ_monoid_delta_dense_thm
|
⊢ ∀ G d
• 0. ∈ G ∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G) ∧ d ∈ G ∧ 0. < d ⇒ (∀ x • 0. < x ⇒ (∃ g• g ∈ G ∧ g ≤ x ∧ x < g + d)) |
ℝ_monoid_dense_thm
|
⊢ ∀ G
• 0. ∈ G ∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G) ∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x)) ⇒ (∀ x y • 0. < x ∧ x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y)) |
ℝ_subgroup_dense_thm
|
⊢ ∀ G
• 0. ∈ G ∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G) ∧ (∀ g• g ∈ G ⇒ ~ g ∈ G) ∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x)) ⇒ (∀ x y• x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y)) |
ℝ_semigroup_dense_thm
|
⊢ ∀ G
• (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G) ∧ (∀ x• 0. < x ⇒ (∃ g• g ∈ G ∧ 0. < g ∧ g < x)) ⇒ (∀ x y • 0. < x ∧ x < y ⇒ (∃ g• g ∈ G ∧ x < g ∧ g < y)) |
ℝ_add_hom_image_group_thm
|
⊢ ∀ f I
• (∀ x y• f (x + y) = f x + f y) ∧ I = {b|∃ a• b = f a} ⇒ 0. ∈ I ∧ (∀ g h• g ∈ I ∧ h ∈ I ⇒ g + h ∈ I) ∧ (∀ g• g ∈ I ⇒ ~ g ∈ I) |
ℝ_add_hom_kernel_group_thm
|
⊢ ∀ f K
• (∀ x y• f (x + y) = f x + f y) ∧ K = {a|f a = 0.} ⇒ 0. ∈ K ∧ (∀ g h• g ∈ K ∧ h ∈ K ⇒ g + h ∈ K) ∧ (∀ g• g ∈ K ⇒ ~ g ∈ K) |
ℝ_opah_thm
|
⊢ ∀ f • (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ (∀ x y• x < y ⇒ f x < f y) |
ℝ_opah_strict_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ (∀ x y• f x < f y ⇒ x < y) |
ℝ_opah_one_one_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ OneOne f |
ℝ_opah_dense_image_thm
|
⊢ ∀ f e
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ∧ 0. < e ⇒ (∃ d• 0. < d ∧ f d < e) |
ℝ_opah_onto_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ Onto f |
ℝ_opah_inverse_add_hom_thm
|
⊢ ∀ f g
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ∧ (∀ x• g (f x) = x) ∧ (∀ x• f (g x) = x) ⇒ (∀ x y• g (x + y) = g x + g y) ∧ (∀ x• 0. < x ⇒ 0. < g x) |
ℝ_opah_inverse_thm
|
⊢ ∀ f
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ (∃ g • (∀ x• g (f x) = x) ∧ (∀ x• f (g x) = x) ∧ (∀ x y• g (x + y) = g x + g y) ∧ (∀ x• 0. < x ⇒ 0. < g x)) |
ℝ_copah_id_thm
|
⊢ ∃ ι
• (∀ x• ι x = x) ∧ (∀ x y• ι (x + y) = ι x + ι y) ∧ (∀ x• 0. < x ⇒ 0. < ι x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• ι (f x) = f (ι x))) |
ℝ_copah_double_thm
|
⊢ ∃ α
• (∀ x• α x = x + x) ∧ (∀ x y• α (x + y) = α x + α y) ∧ (∀ x• 0. < x ⇒ 0. < α x) ∧ (∀ x• 0. < x ⇒ x < α x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• α (f x) = f (α x))) |
ℝ_copah_halve_thm
|
⊢ ∃ β
• (∀ x• β x + β x = x) ∧ (∀ x y• β (x + y) = β x + β y) ∧ (∀ x• 0. < x ⇒ 0. < β x) ∧ (∀ x• 0. < x ⇒ β x < x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• β (f x) = f (β x))) |
ℝ_copah_comp_thm
|
⊢ ∀ α β
• (∀ x y• α (x + y) = α x + α y) ∧ (∀ x• 0. < x ⇒ 0. < α x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• α (f x) = f (α x))) ∧ (∀ x y• β (x + y) = β x + β y) ∧ (∀ x• 0. < x ⇒ 0. < β x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• β (f x) = f (β x))) ⇒ (∃ γ • (∀ x• γ x = α (β x)) ∧ (∀ x• 0. < x ⇒ 0. < γ x) ∧ (∀ x y• γ (x + y) = γ x + γ y) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• γ (f x) = f (γ x)))) |
ℝ_copah_sum_thm
|
⊢ ∀ α β
• (∀ x y• α (x + y) = α x + α y) ∧ (∀ x• 0. < x ⇒ 0. < α x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• α (f x) = f (α x))) ∧ (∀ x y• β (x + y) = β x + β y) ∧ (∀ x• 0. < x ⇒ 0. < β x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• β (f x) = f (β x))) ⇒ (∃ γ • (∀ x• γ x = α x + β x) ∧ (∀ x• 0. < x ⇒ 0. < γ x) ∧ (∀ x y• γ (x + y) = γ x + γ y) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• γ (f x) = f (γ x)))) |
ℝ_halve_closed_dense_thm
|
⊢ ∀ A e
• 0. < e ∧ e ∈ A ∧ (∀ y• y ∈ A ⇒ (∃ z• z ∈ A ∧ z + z = y)) ⇒ (∀ d• 0. < d ⇒ (∃ a• a ∈ A ∧ 0. < a ∧ a < d)) |
ℝ_copah_dense_thm
|
⊢ ∀ d x y
• 0. < d ∧ 0. < x ∧ x < y ⇒ (∃ γ • (∀ x y• γ (x + y) = γ x + γ y) ∧ (∀ x• 0. < x ⇒ 0. < γ x) ∧ (∀ f • (∀ x y• f (x + y) = f x + f y) ⇒ (∀ x• γ (f x) = f (γ x))) ∧ x < γ d ∧ γ d < y) |
ℝ_opah_extension_thm1
|
⊢ ∀ f
• (∀ x y• 0. < x ∧ 0. < y ⇒ f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ (∃ φ • φ 0. = 0. ∧ (∀ x• 0. < x ⇒ φ x = f x) ∧ (∀ x y • 0. ≤ x ∧ 0. ≤ y ⇒ φ (x + y) = φ x + φ y)) |
ℝ_opah_extension_thm2
|
⊢ ∀ f
• f 0. = 0. ∧ (∀ x y • 0. ≤ x ∧ 0. ≤ y ⇒ f (x + y) = f x + f y) ⇒ (∃ ψ • (∀ x• 0. ≤ x ⇒ ψ x = f x) ∧ (∀ x y• ψ (x + y) = ψ x + ψ y)) |
ℝ_opah_extension_thm
|
⊢ ∀ f
• (∀ x y• 0. < x ∧ 0. < y ⇒ f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ⇒ (∃ φ • (∀ x• 0. < x ⇒ φ x = f x) ∧ (∀ x y• φ (x + y) = φ x + φ y) ∧ (∀ x• 0. < x ⇒ 0. < φ x)) |
ℝ_opah_order_thm
|
⊢ ∀ f g d
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ∧ (∀ x y• g (x + y) = g x + g y) ∧ (∀ x• 0. < x ⇒ 0. < g x) ∧ 0. < d ∧ f d < g d ⇒ (∀ x• 0. < x ⇒ f x < g x) |
ℝ_opah_eq_thm
|
⊢ ∀ f g d
• (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ∧ (∀ x y• g (x + y) = g x + g y) ∧ (∀ x• 0. < x ⇒ 0. < g x) ∧ 0. < d ∧ f d = g d ⇒ f = g |
ℝ_opah_complete_thm
|
⊢ ∀ d e
• 0. < d ∧ 0. < e ⇒ (∃ f • (∀ x y• f (x + y) = f x + f y) ∧ (∀ x• 0. < x ⇒ 0. < f x) ∧ f d = e) |
*R_consistent
|
⊢ Consistent
(λ *R' • (∀ x y z • *R' (*R' x y) z = *R' x (*R' y z)) ∧ (∀ x• *R' x 1. = x) ∧ (∀ x y z • *R' x (y + z) = *R' x y + *R' x z) ∧ (∀ x y• *R' x y = *R' y x) ∧ (∀ 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
• x * (y + z) = x * y + x * z ∧ (x + y) * z = x * z + y * z |
ℝ_times_order_thm
|
⊢ ∀ x y z
• y * x = x * y ∧ (x * y) * z = x * y * z ∧ 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
• ~ x * y = ~ (x * y) ∧ x * ~ y = ~ (x * y) ∧ ~ x * ~ y = x * y |
/R_consistent
|
⊢ Consistent
(λ /R' • (∀ y z• ¬ z = 0. ⇒ /R' (y * z) z = y) ∧ (∀ x y z • ¬ 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
• 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.
∧ (∀ w • ¬ w = 0. ⇒ w -1 -1 = w ∧ w * w -1 = 1. ∧ w -1 * w = 1.)) ∧ (∀ w z • ¬ w = 0. ∧ ¬ z = 0. ⇒ (w * z) -1 = w -1 * z -1) |
ℝ_cross_mult_eq_thm
|
⊢ ∀ w z
• ¬ w = 0. ∧ ¬ z = 0. ⇒ (∀ 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
• 0. < w ∧ 0. < z ⇒ (∀ x y• x / w < y / z ⇔ x * z < w * y) |
ℝ_over_cancel_eq_thm
|
⊢ ∀ w z
• ¬ w = 0. ∧ ¬ z = 0. ⇒ (∀ x• (x * z) / (w * z) = x / w) |
ℝ_over_plus_over_thm
|
⊢ ∀ x y u v
• ¬ u = 0. ∧ ¬ v = 0. ⇒ 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
• i / (m + 1) = j / (n + 1) ⇔ i * (n + 1) = j * (m + 1) |
ℝ_frac_cancel_eq_thm
|
⊢ ∀ i m n
• (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
• i / (m + 1) + j / (n + 1) = (i * (n + 1) + j * (m + 1)) / ((m + 1) * (n + 1)) |
ℝ_frac_minus_frac_thm
|
⊢ ∀ i j k m n
• j * (m + 1) ≤ i * (n + 1) ⇒ i / (m + 1) + ~ (j / (n + 1)) = (i * (n + 1) - j * (m + 1)) / ((m + 1) * (n + 1)) |
ℝ_frac_minus_frac_thm1
|
⊢ ∀ i j m n
• i * (n + 1) ≤ j * (m + 1) ⇒ i / (m + 1) + ~ (j / (n + 1)) = ~ ((j * (m + 1) - i * (n + 1)) / ((m + 1) * (n + 1))) |
ℝ_over_times_over_thm
|
⊢ ∀ x y u v
• ¬ u = 0. ∧ ¬ v = 0. ⇒ x / u * y / v = (x * y) / (u * v) |
ℝ_frac_times_frac_thm
|
⊢ ∀ i j m n
• i / (m + 1) * j / (n + 1) = (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
• ¬ u = 0. ∧ ¬ v = 0. ∧ ¬ y = 0. ⇒ x / u / (y / v) = (x * v) / (u * y) |
ℝ_frac_less_frac_thm
|
⊢ ∀ i j m n
• i / (m + 1) < j / (n + 1) ⇔ 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
(λ MaxR' • (∀ x• MaxR' [x] = x) ∧ (∀ x y L • MaxR' (Cons x (Cons y L)) = (if x < MaxR' (Cons y L) then MaxR' (Cons y L) else x))) |
MinR_consistent
|
⊢ Consistent
(λ MinR' • (∀ x• MinR' [x] = x) ∧ (∀ x y L • MinR' (Cons x (Cons y L)) = (if x > MinR' (Cons y L) then MinR' (Cons y L) else x))) |
ℝ_max_cons_thm
|
⊢ ∀ x L
• MaxR (Cons x L) = (if L = [] then x else if x < MaxR L then MaxR L else x) |
ℝ_max_conv_thm
|
⊢ ∀ x y L
• MaxR (Cons x (Cons y L)) = (if x < y then MaxR (Cons y L) else MaxR (Cons x L)) |
ℝ_min_cons_thm
|
⊢ ∀ x L
• MinR (Cons x L) = (if L = [] then x else if MinR L < x then MinR L else x) |
ℝ_min_conv_thm
|
⊢ ∀ x y L
• MinR (Cons x (Cons y L)) = (if x < y then MinR (Cons x L) else MinR (Cons y L)) |
^Z_consistent
|
⊢ Consistent
(λ ^Z' • ∀ x m • ^Z' x (ℕℤ m) = x ^ m ∧ ^Z' x (~ (ℕℤ (m + 1))) = (x ^ (m + 1)) -1) |
ℤℝ_consistent
|
⊢ Consistent
(λ $"ℤℝ'" • $"ℤℝ'" (ℕℤ 0) = 0. ∧ $"ℤℝ'" (ℕℤ 1) = 1. ∧ (∀ i j • $"ℤℝ'" (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 |