The Theory analysis
Parents
fin_set
Children
group_egs metric_spaces fincomb
Constants
PolyFunc
(ℝ → ℝ) ℘
PolyEval
ℝ LIST → ℝ → ℝ
PlusCoeffs
ℝ LIST → ℝ LIST → ℝ LIST
TimesCoeffs
ℝ LIST → ℝ LIST → ℝ LIST
$To
(ℕ → 'a) → ℕ → 'a LIST
Roots
('a → ℝ) → 'a ℘
$->
(ℕ → ℝ) → ℝ → BOOL
ClosedInterval
ℝ → ℝ → ℝ ℘
OpenInterval
ℝ → ℝ → ℝ ℘
$Cts
(ℝ → ℝ) → ℝ → BOOL
$Deriv
(ℝ → ℝ) → ℝ → ℝ → BOOL
DerivCoeffs
ℝ LIST → ℝ LIST
OpenR
ℝ ℘ ℘
ClosedR
ℝ ℘ ℘
CompactR
ℝ ℘ ℘
$-->
(ℝ → ℝ) → ℝ → ℝ → BOOL
$--->
(ℕ → ℝ → ℝ) → (ℝ → ℝ) → ℝ ℘ → BOOL
Series
(ℕ → ℝ) → ℕ → ℝ
PowerSeries
(ℕ → ℝ) → ℕ → ℝ → ℝ
$!
ℕ → ℕ
Exp
ℝ → ℝ
Log
ℝ → ℝ
Cos
ℝ → ℝ
Sin
ℝ → ℝ
ArchimedesConstant
$+#->
(ℝ → ℝ) → ℝ → ℝ → BOOL
$-+#>
(ℝ → ℝ) → ℝ → BOOL
$-+#>+#
(ℝ → ℝ) → BOOL
Sqrt
ℝ → ℝ
Tan
ℝ → ℝ
Cotan
ℝ → ℝ
Sec
ℝ → ℝ
Cosec
ℝ → ℝ
ArcSin
ℝ → ℝ
ArcCos
ℝ → ℝ
Sinh
ℝ → ℝ
Cosh
ℝ → ℝ
Tanh
ℝ → ℝ
Cotanh
ℝ → ℝ
Sech
ℝ → ℝ
Cosech
ℝ → ℝ
ArcSinh
ℝ → ℝ
TaggedPartition
(ℕ → ℝ) ↔ ((ℕ → ℝ) × ℕ)
RiemannSum
(ℝ → ℝ) → (ℕ → ℝ) × (ℕ → ℝ) × ℕ → ℝ
Gauge
(ℝ → ℝ ℘) ℘
$Fine
(ℝ → ℝ ℘) → (ℕ → ℝ) ↔ ((ℕ → ℝ) × ℕ)
$IntR
(ℝ → ℝ) → ℝ → BOOL
CharFun
'a ℘ → 'a → ℝ
$Int
(ℝ → ℝ) → ℝ → ℝ ℘ → BOOL
$Area
ℝ ↔ ℝ → ℝ → BOOL
Aliases
π
ArchimedesConstant : ℝ
χ
CharFun : 'a ℘ → 'a → ℝ
Fixity
Right Infix 200:
Area Cts Deriv Int IntR ->
Right Infix 205:
+#-> -+#> ---> -->
Right Infix 310:
To
Postfix 200: -+#>+#
Postfix 330: Fine !
Definitions
PolyFunc
⊢ PolyFunc
fill= ⋂
fill{A
fill|(∀ c• (λ x• c) ∈ A)
fill∧ (λ x• x) ∈ A
fill∧ (∀ f g
fill• f ∈ A ∧ g ∈ A ⇒ (λ x• f x + g x) ∈ A)
fill∧ (∀ f g
fill• f ∈ A ∧ g ∈ A ⇒ (λ x• f x * g x) ∈ A)}
PolyEval
⊢ (∀ x• PolyEval [] x = 0.)
fill∧ (∀ c l x
fill• PolyEval (Cons c l) x = c + x * PolyEval l x)
PlusCoeffs
⊢ ConstSpec
fill(λ PlusCoeffs'
fill• (∀ l• PlusCoeffs' [] l = l)
fill∧ (∀ l• PlusCoeffs' l [] = l)
fill∧ (∀ c1 l1 c2 l2
fill• PlusCoeffs' (Cons c1 l1) (Cons c2 l2)
fill= Cons (c1 + c2) (PlusCoeffs' l1 l2)))
fillPlusCoeffs
TimesCoeffs
⊢ (∀ l• TimesCoeffs [] l = [])
fill∧ (∀ c l1 l2
fill• TimesCoeffs (Cons c l1) l2
fill= PlusCoeffs
fill(Cons 0. (TimesCoeffs l1 l2))
fill(Map (λ x• c * x) l2))
To
⊢ (∀ f• f To 0 = [])
fill∧ (∀ f n• f To (n + 1) = f To n ⁀ [f n])
Roots
⊢ ∀ f• Roots f = {x|f x = 0.}
->
⊢ ∀ s x
fill• s -> x
fill⇔ (∀ e
fill• 0. < e ⇒ (∃ n• ∀ m• n ≤ m ⇒ Abs (s m - x) < e))
ClosedInterval
⊢ ∀ x y• ClosedInterval x y = {t|x ≤ t ∧ t ≤ y}
OpenInterval
⊢ ∀ x y• OpenInterval x y = {t|x < t ∧ t < y}
Cts
⊢ ∀ f x
fill• f Cts x
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ d
fill• 0. < d
fill∧ (∀ y
fill• Abs (y - x) < d
fill⇒ Abs (f y - f x) < e)))
Deriv
⊢ ∀ f c x
fill• (f Deriv c) x
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ d
fill• 0. < d
fill∧ (∀ y
fill• Abs (y - x) < d ∧ ¬ y = x
fill⇒ Abs ((f y - f x) / (y - x) - c)
fill< e)))
DerivCoeffs
⊢ DerivCoeffs [] = []
fill∧ (∀ c l
fill• DerivCoeffs (Cons c l)
fill= PlusCoeffs l (Cons 0. (DerivCoeffs l)))
OpenR
⊢ OpenR
fill= {A
fill|∀ t
fill• t ∈ A
fill⇒ (∃ x y
fill• t ∈ OpenInterval x y
fill∧ OpenInterval x y ⊆ A)}
ClosedR
⊢ ClosedR = {A|~ A ∈ OpenR}
CompactR
⊢ CompactR
fill= {A
fill|∀ V
fill• V ⊆ OpenR ∧ A ⊆ ⋃ V
fill⇒ (∃ W• W ⊆ V ∧ W ∈ Finite ∧ A ⊆ ⋃ W)}
-->
⊢ ∀ f c x
fill• (f --> c) x
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ d
fill• 0. < d
fill∧ (∀ y
fill• Abs (y - x) < d ∧ ¬ y = x
fill⇒ Abs (f y - c) < e)))
--->
⊢ ∀ u h X
fill• (u ---> h) X
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ m y
fill• n ≤ m ∧ y ∈ X ⇒ Abs (u m y - h y) < e))
Series
⊢ (∀ s• Series s 0 = 0.)
fill∧ (∀ s n• Series s (n + 1) = Series s n + s n)
PowerSeries
⊢ ∀ s n• PowerSeries s n = PolyEval (s To n)
!
⊢ 0 ! = 1 ∧ (∀ m• (m + 1) ! = (m + 1) * m !)
Exp
⊢ ConstSpec
fill(λ Exp'
fill• Exp' 0. = 1. ∧ (∀ x• (Exp' Deriv Exp' x) x))
fillExp
Log
⊢ ConstSpec (λ Log'• ∀ x• Log' (Exp x) = x) Log
Sin
Cos
⊢ ConstSpec
fill(λ (Sin', Cos')
fill• Sin' 0. = 0.
fill∧ Cos' 0. = 1.
fill∧ (∀ x• (Sin' Deriv Cos' x) x)
fill∧ (∀ x• (Cos' Deriv ~ (Sin' x)) x))
fill(Sin, Cos)
ArchimedesConstant
⊢ ConstSpec
fill(λ ArchimedesConstant'
fill• 0. < ArchimedesConstant'
fill∧ (∀ x
fill• Sin x = 0.
fill⇔ (∃ m• x = ℕℝ m * ArchimedesConstant')
fill∨ (∃ m
fill• x = ~ (ℕℝ m * ArchimedesConstant'))))
fillπ
+#->
⊢ ∀ f c a
fill• (f +#-> c) a
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ b
fill• a < b
fill∧ (∀ x
fill• a < x ∧ x < b ⇒ Abs (f x - c) < e)))
-+#>
⊢ ∀ f c
fill• f -+#> c
fill⇔ (∀ e
fill• 0. < e ⇒ (∃ b• ∀ x• b < x ⇒ Abs (f x - c) < e))
-+#>+#
⊢ ∀ f• f -+#>+# ⇔ (∀ x• ∃ b• ∀ y• b < y ⇒ x < f y)
Sqrt
⊢ ConstSpec
fill(λ Sqrt'
fill• ∀ x
fill• 0. ≤ x
fill⇒ 0. ≤ Sqrt' x
fill∧ Sqrt' x ^ 2 = x
fill∧ Sqrt' Cts x)
fillSqrt
Tan
⊢ ∀ x• Tan x = Sin x * Cos x -1
Cotan
⊢ ∀ x• Cotan x = Cos x * Sin x -1
Sec
⊢ ∀ x• Sec x = Cos x -1
Cosec
⊢ ∀ x• Cosec x = Sin x -1
ArcSin
⊢ ConstSpec
fill(λ ArcSin'
fill• (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin' (Sin x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1.
fill⇒ Sin (ArcSin' x) = x ∧ ArcSin' Cts x))
fillArcSin
ArcCos
⊢ ConstSpec
fill(λ ArcCos'
fill• (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos' (Cos x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1.
fill⇒ Cos (ArcCos' x) = x ∧ ArcCos' Cts x))
fillArcCos
Sinh
⊢ ∀ x• Sinh x = 1 / 2 * (Exp x - Exp (~ x))
Cosh
⊢ ∀ x• Cosh x = 1 / 2 * (Exp x + Exp (~ x))
Tanh
⊢ ∀ x• Tanh x = Sinh x * Cosh x -1
Cotanh
⊢ ∀ x• Cotanh x = Cosh x * Sinh x -1
Sech
⊢ ∀ x• Sech x = Cosh x -1
Cosech
⊢ ∀ x• Cosech x = Sinh x -1
ArcSinh
⊢ ConstSpec
fill(λ ArcSinh'
fill• ∀ x
fill• ArcSinh' (Sinh x) = x
fill∧ Sinh (ArcSinh' x) = x
fill∧ ArcSinh' Cts x)
fillArcSinh
TaggedPartition
⊢ ∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill⇔ (∀ m• m < n ⇒ I m < I (m + 1))
fill∧ (∀ m
fill• m < n
fill⇒ t m ∈ ClosedInterval (I m) (I (m + 1)))
RiemannSum
⊢ ∀ f t I n
fill• RiemannSum f (t, I, n)
fill= Series (λ m• f (t m) * (I (m + 1) - I m)) n
Gauge
⊢ ∀ G• G ∈ Gauge ⇔ (∀ x• G x ∈ OpenR ∧ x ∈ G x)
Fine
⊢ ∀ t I n G
fill• (t, I, n) ∈ G Fine
fill⇔ (∀ m
fill• m < n
fill⇒ ClosedInterval (I m) (I (m + 1)) ⊆ G (t m))
IntR
⊢ ∀ f c
fill• f IntR c
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G a b
fill• G ∈ Gauge
fill∧ a < b
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 < a
fill∧ b < I n
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e)))
CharFun
⊢ ∀ A x• χ A x = (if x ∈ A then 1. else 0.)
Int
⊢ ∀ f c A• (f Int c) A ⇔ (λ x• χ A x * f x) IntR c
Area
⊢ ∀ A c
fill• A Area c
fill⇔ (∃ sf
fill• sf IntR c
fill∧ (∀ x• χ {y|(x, y) ∈ A} IntR sf x))
Theorems
PlusCoeffs_consistent
⊢ Consistent
fill(λ PlusCoeffs'
fill• (∀ l• PlusCoeffs' [] l = l)
fill∧ (∀ l• PlusCoeffs' l [] = l)
fill∧ (∀ c1 l1 c2 l2
fill• PlusCoeffs' (Cons c1 l1) (Cons c2 l2)
fill= Cons (c1 + c2) (PlusCoeffs' l1 l2)))
plus_coeffs_def
⊢ (∀ l• PlusCoeffs [] l = l)
fill∧ (∀ l• PlusCoeffs l [] = l)
fill∧ (∀ c1 l1 c2 l2
fill• PlusCoeffs (Cons c1 l1) (Cons c2 l2)
fill= Cons (c1 + c2) (PlusCoeffs l1 l2))
const_eval_thm
⊢ ∀ c• (λ x• c) = PolyEval [c]
id_eval_thm
⊢ (λ x• x) = PolyEval [0.; 1.]
plus_eval_thm
⊢ ∀ l1 l2
fill• (λ x• PolyEval l1 x + PolyEval l2 x)
fill= PolyEval (PlusCoeffs l1 l2)
const_times_eval_thm
⊢ ∀ c l
fill• (λ x• c * PolyEval l x)
fill= PolyEval (Map (λ y• c * y) l)
times_eval_thm
⊢ ∀ l1 l2
fill• (λ x• PolyEval l1 x * PolyEval l2 x)
fill= PolyEval (TimesCoeffs l1 l2)
poly_induction_thm
⊢ ∀ p
fill• (∀ c• p (λ x• c))
fill∧ p (λ x• x)
fill∧ (∀ f g• p f ∧ p g ⇒ p (λ x• f x + g x))
fill∧ (∀ f g• p f ∧ p g ⇒ p (λ x• f x * g x))
fill⇒ (∀ h• h ∈ PolyFunc ⇒ p h)
poly_func_eq_poly_eval_thm
⊢ PolyFunc = {f|∃ l• f = PolyEval l}
const_poly_func_thm
⊢ ∀ c• (λ x• c) ∈ PolyFunc
id_poly_func_thm
⊢ (λ x• x) ∈ PolyFunc
plus_poly_func_thm
⊢ ∀ f g
fill• f ∈ PolyFunc ∧ g ∈ PolyFunc
fill⇒ (λ x• f x + g x) ∈ PolyFunc
times_poly_func_thm
⊢ ∀ f g
fill• f ∈ PolyFunc ∧ g ∈ PolyFunc
fill⇒ (λ x• f x * g x) ∈ PolyFunc
comp_poly_func_thm
⊢ ∀ f g
fill• f ∈ PolyFunc ∧ g ∈ PolyFunc
fill⇒ (λ x• f (g x)) ∈ PolyFunc
poly_eval_append_thm
⊢ ∀ l1 l2 x
fill• PolyEval (l1 ⁀ l2) x
fill= PolyEval l1 x + x ^ # l1 * PolyEval l2 x
poly_eval_rev_thm
⊢ (∀ x• PolyEval (Rev []) x = 0.)
fill∧ (∀ c l x
fill• PolyEval (Rev (Cons c l)) x
fill= c * x ^ # l + PolyEval (Rev l) x)
poly_diff_powers_thm
⊢ ∀ n x y
fill• (x - y)
fill* PolyEval (Rev ((λ m• y ^ m) To (n + 1))) x
fill= x ^ (n + 1) - y ^ (n + 1)
length_plus_coeffs_thm
⊢ ∀ l1 l2
fill• # (PlusCoeffs l1 l2)
fill= (if # l2 < # l1 then # l1 else # l2)
poly_linear_div_thm
⊢ ∀ l1 c
fill• ¬ l1 = []
fill⇒ (∃ l2 r
fill• # l2 < # l1
fill∧ (λ x• PolyEval l1 x)
fill= (λ x• (x - c) * PolyEval l2 x + r))
poly_remainder_thm
⊢ ∀ l1 c
fill• ¬ l1 = []
fill⇒ (∃ l2
fill• # l2 < # l1
fill∧ (λ x• PolyEval l1 x)
fill= (λ x
fill• (x - c) * PolyEval l2 x + PolyEval l1 c))
poly_factor_thm
⊢ ∀ l1 c
fill• ¬ l1 = [] ∧ PolyEval l1 c = 0.
fill⇒ (∃ l2
fill• # l2 < # l1
fill∧ (λ x• PolyEval l1 x)
fill= (λ x• (x - c) * PolyEval l2 x))
poly_roots_finite_thm
⊢ ∀ f c• f ∈ PolyFunc ∧ ¬ f c = 0. ⇒ Roots f ∈ Finite
ℝ_0_≤_abs_thm
⊢ ∀ x• 0. ≤ Abs x
ℝ_abs_plus_thm
⊢ ∀ x y• Abs (x + y) ≤ Abs x + Abs y
ℝ_abs_subtract_thm
⊢ ∀ x y• Abs (x - y) ≤ Abs x + Abs y
ℝ_abs_plus_minus_thm
⊢ ∀ x y• Abs (x + ~ y) ≤ Abs x + Abs y
ℝ_abs_diff_bounded_thm
⊢ ∀ x y z
fill• 0. < z
fill⇒ (Abs (x + ~ y) < z ⇔ y + ~ z < x ∧ x < y + z)
ℝ_abs_plus_bc_thm
⊢ ∀ x y z• Abs x ≤ Abs (y + z) ⇒ Abs x ≤ Abs y + Abs z
ℝ_abs_abs_minus_thm
⊢ ∀ x y• Abs (Abs x - Abs y) ≤ Abs (x - y)
ℝ_abs_abs_thm
⊢ ∀ x• Abs (Abs x) = Abs x
ℝ_abs_times_thm
⊢ ∀ x y• Abs (x * y) = Abs x * Abs y
ℝ_abs_ℝ_ℕ_exp_thm
⊢ ∀ x m• Abs (x ^ m) = Abs x ^ m
ℝ_abs_eq_0_thm
⊢ ∀ x• Abs x = 0. ⇔ x = 0.
ℝ_abs_≤_0_thm
⊢ ∀ x• Abs x ≤ 0. ⇔ x = 0.
ℝ_abs_0_thm
⊢ Abs 0. = 0.
ℝ_abs_recip_thm
⊢ ∀ x• ¬ x = 0. ⇒ Abs (x -1) = Abs x -1
ℝ_abs_squared_thm
⊢ ∀ x• Abs x ^ 2 = x ^ 2
ℝ_abs_less_times_thm
⊢ ∀ x t y u
fill• Abs x < t ∧ Abs y < u ⇒ Abs x * Abs y < t * u
ℝ_¬_0_abs_thm
⊢ ∀ x• ¬ x = 0. ⇔ 0. < Abs x
ℝ_less_recip_less_thm
⊢ ∀ x y• 0. < x ∧ x < y ⇒ y -1 < x -1
ℝ_abs_≤_less_interval_thm
⊢ ∀ x y
fill• (Abs x ≤ y ⇔ x ∈ ClosedInterval (~ y) y)
fill∧ (Abs x < y ⇔ x ∈ OpenInterval (~ y) y)
ℝ_plus_recip_thm
⊢ ∀ x y
fill• ¬ x = 0. ∧ ¬ y = 0.
fill⇒ x -1 + y -1 = (x + y) * x -1 * y -1
ℕℝ_recip_thm
⊢ ∀ m• ℕℝ (m + 1) -1 -1 = ℕℝ (m + 1)
ℕℝ_0_less_recip_thm
⊢ ∀ m• 0. < ℕℝ (m + 1) -1
ℕℝ_recip_not_eq_0_thm
⊢ ∀ m• ¬ ℕℝ (m + 1) -1 = 0.
ℝ_ℕ_exp_0_1_thm
⊢ ∀ m• 0. ^ (m + 1) = 0. ∧ 1. ^ m = 1.
ℝ_ℕ_exp_square_thm
⊢ ∀ x• x ^ 2 = x * x
ℝ_ℕ_exp_0_less_thm
⊢ ∀ m x• 0. < x ⇒ 0. < x ^ m
ℝ_ℕ_exp_1_less_mono_thm
⊢ ∀ x m• 1. < x ⇒ x ^ m < x ^ (m + 1)
ℝ_ℕ_exp_1_less_mono_thm1
⊢ ∀ x m n• 1. < x ∧ m < n ⇒ x ^ m < x ^ n
ℝ_≤_times_mono_thm
⊢ ∀ x y z• 0. ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
ℝ_ℕ_exp_¬_eq_0_thm
⊢ ∀ m x• ¬ x = 0. ⇒ ¬ x ^ m = 0.
ℝ_ℕ_exp_plus_thm
⊢ ∀ x m n• x ^ (m + n) = x ^ m * x ^ n
ℝ_ℕ_exp_times_thm
⊢ ∀ x y m• (x * y) ^ m = x ^ m * y ^ m
ℝ_ℕ_exp_recip_thm
⊢ ∀ m x• ¬ x = 0. ⇒ (x ^ m) -1 = (x -1) ^ m
ℝ_ℕ_exp_recip_thm1
⊢ ∀ m x• ¬ x = 0. ⇒ (x -1) ^ m = (x ^ m) -1
ℝ_ℕ_exp_1_≤_thm
⊢ ∀ m x• 1. ≤ x ⇒ 1. ≤ x ^ m
ℝ_ℕ_exp_less_1_mono_thm
⊢ ∀ x m• 0. < x ∧ x < 1. ⇒ x ^ (m + 1) < x ^ m
ℝ_ℕ_exp_less_mono_thm
⊢ ∀ x m• 0. < x ⇒ 0. < x ^ m
ℝ_ℕ_exp_less_1_mono_thm1
⊢ ∀ x m n• 0. < x ∧ x < 1. ∧ m < n ⇒ x ^ n < x ^ m
ℝ_ℕ_exp_linear_estimate_thm
⊢ ∀ x m• 0. < x ⇒ 1. + ℕℝ m * x ≤ (1. + x) ^ m
ℝ_0_≤_square_thm
⊢ ∀ x• 0. ≤ x ^ 2
ℝ_square_eq_0_thm
⊢ ∀ x• x ^ 2 = 0. ⇔ x = 0.
ℝ_bound_below_2_thm
⊢ ∀ x y
fill• 0. < x ∧ 0. < y ⇒ (∃ d• 0. < d ∧ d < x ∧ d < y)
ℝ_bound_below_3_thm
⊢ ∀ x y z
fill• 0. < x ∧ 0. < y ∧ 0. < z
fill⇒ (∃ d• 0. < d ∧ d < x ∧ d < y ∧ d < z)
ℝ_max_2_thm
⊢ ∀ x y• ∃ z• x < z ∧ y < z
ℝ_max_3_thm
⊢ ∀ x y z• ∃ t• x < t ∧ y < t ∧ z < t
ℝ_min_2_thm
⊢ ∀ x y• ∃ z• z < x ∧ z < y
ℝ_min_3_thm
⊢ ∀ x y z• ∃ t• t < x ∧ t < y ∧ t < z
ℝ_archimedean_thm
⊢ ∀ x• ∃ m• x < ℕℝ m
ℝ_archimedean_recip_thm
⊢ ∀ x• 0. < x ⇒ (∃ m• ℕℝ (m + 1) -1 < x)
ℝ_archimedean_times_thm
⊢ ∀ x y• 0. < x ⇒ (∃ m• y < ℕℝ m * x)
ℝ_archimedean_division_thm
⊢ ∀ d y
fill• 0. < d ∧ 0. ≤ y
fill⇒ (∃ q r• y = ℕℝ q * d + r ∧ 0. ≤ r ∧ r < d)
ℝ_ℕ_exp_tends_to_infinity_thm
⊢ ∀ x y• 1. < x ⇒ (∃ m• y < x ^ m)
ℝ_ℕ_exp_tends_to_0_thm
⊢ ∀ x y• 0. < x ∧ x < 1. ∧ 0. < y ⇒ (∃ m• x ^ m < y)
const_lim_seq_thm
⊢ ∀ c• (λ m• c) -> c
plus_lim_seq_thm
⊢ ∀ s1 c1 s2 c2
fill• s1 -> c1 ∧ s2 -> c2 ⇒ (λ m• s1 m + s2 m) -> c1 + c2
lim_seq_bounded_thm
⊢ ∀ s c• s -> c ⇒ (∃ b• 0. < b ∧ (∀ m• Abs (s m) < b))
times_lim_seq_thm
⊢ ∀ s1 c1 s2 c2
fill• s1 -> c1 ∧ s2 -> c2 ⇒ (λ m• s1 m * s2 m) -> c1 * c2
minus_lim_seq_thm
⊢ ∀ s c• s -> c ⇔ (λ m• ~ (s m)) -> ~ c
poly_lim_seq_thm
⊢ ∀ f s t
fill• f ∈ PolyFunc ∧ s -> t ⇒ (λ x• f (s x)) -> f t
recip_lim_seq_thm
⊢ ∀ s t• s -> t ∧ ¬ t = 0. ⇒ (λ m• s m -1) -> t -1
lim_seq_choice_thm
⊢ ∀ p s1 s2 x
fill• s1 -> x ∧ s2 -> x
fill⇒ (λ m• if p m then s1 m else s2 m) -> x
abs_lim_seq_thm
⊢ ∀ s x• s -> x ⇒ (λ m• Abs (s m)) -> Abs x
lim_seq_recip_ℕ_thm
⊢ ∀ x• (λ m• x + ℕℝ (m + 1) -1) -> x
lim_seq_¬_eq_thm
⊢ ∀ x• ∃ s• s -> x ∧ (∀ m• ¬ s m = x)
lim_seq_shift_thm
⊢ ∀ m s x• s -> x ⇔ (λ n• s (n + m)) -> x
lim_seq_¬_eq_thm1
⊢ ∀ x d
fill• 0. < d
fill⇒ (∃ s
fill• s -> x ∧ (∀ m• Abs (s m - x) < d ∧ ¬ s m = x))
lim_seq_¬_0_thm
⊢ ∀ s x
fill• s -> x ∧ ¬ x = 0. ⇒ (∃ n• ∀ m• n ≤ m ⇒ ¬ s m = 0.)
lim_seq_upper_bound_thm
⊢ ∀ s b c• (∀ m• s m ≤ b) ∧ s -> c ⇒ c ≤ b
lim_seq_unique_thm
⊢ ∀ s b c• s -> b ∧ s -> c ⇒ b = c
lim_seq_diffs_tend_to_0_thm
⊢ ∀ s c• s -> c ⇒ (λ m• s (m + 1) - s m) -> 0.
cts_lim_seq_thm
⊢ ∀ f x
fill• f Cts x ⇔ (∀ s• s -> x ⇒ (λ m• f (s m)) -> f x)
cts_lim_seq_thm1
⊢ ∀ f x
fill• f Cts x
fill⇔ (∀ s
fill• s -> x ∧ (∀ m• ¬ s m = x)
fill⇒ (λ m• f (s m)) -> f x)
cts_lim_seq_thm2
⊢ ∀ f x
fill• f Cts x
fill⇔ (∃ a b
fill• a < x
fill∧ x < b
fill∧ (∀ s
fill• s -> x
fill∧ (∀ m• ¬ s m = x ∧ a < s m ∧ s m < b)
fill⇒ (λ m• f (s m)) -> f x))
cts_local_thm
⊢ ∀ f g x a b
fill• a < x
fill∧ x < b
fill∧ (∀ y• a < y ∧ y < b ⇒ f y = g y)
fill∧ g Cts x
fill⇒ f Cts x
const_cts_thm
⊢ ∀ c t• (λ x• c) Cts t
id_cts_thm
⊢ ∀ t• (λ x• x) Cts t
plus_cts_thm
⊢ ∀ f g t• f Cts t ∧ g Cts t ⇒ (λ x• f x + g x) Cts t
times_cts_thm
⊢ ∀ f g t• f Cts t ∧ g Cts t ⇒ (λ x• f x * g x) Cts t
poly_cts_thm
⊢ ∀ f t• f ∈ PolyFunc ⇒ f Cts t
comp_cts_thm
⊢ ∀ f g t• f Cts g t ∧ g Cts t ⇒ (λ x• f (g x)) Cts t
minus_cts_thm
⊢ ∀ t• ~ Cts t
minus_comp_cts_thm
⊢ ∀ f t• f Cts t ⇒ (λ x• ~ (f x)) Cts t
recip_cts_thm
⊢ ∀ t• ¬ t = 0. ⇒ $-1 Cts t
recip_comp_cts_thm
⊢ ∀ f t• f Cts t ∧ ¬ f t = 0. ⇒ (λ x• f x -1) Cts t
ℝ_ℕ_exp_cts_thm
⊢ ∀ m t• (λ x• x ^ m) Cts t
ℝ_ℕ_exp_comp_cts_thm
⊢ ∀ f m t• f Cts t ⇒ (λ x• f x ^ m) Cts t
abs_cts_thm
⊢ ∀ t• Abs Cts t
abs_comp_cts_thm
⊢ ∀ f m t• f Cts t ⇒ (λ x• Abs (f x)) Cts t
cts_extension_thm1
⊢ ∀ a b f
fill• a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill⇒ (∃ g
fill• (∀ x• a ≤ x ∧ x ≤ b ⇒ g x = f x)
fill∧ (∀ x• x < a ⇒ g x = f a)
fill∧ (∀ x• b < x ⇒ g x = f b)
fill∧ (∀ x• g Cts x))
cts_extension_thm
⊢ ∀ a b f
fill• a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill⇒ (∃ g
fill• (∀ x• a ≤ x ∧ x ≤ b ⇒ g x = f x)
fill∧ (∀ x• g Cts x))
open_ℝ_delta_thm
⊢ ∀ A
fill• A ∈ OpenR
fill⇔ (∀ t
fill• t ∈ A
fill⇒ (∃ d
fill• 0. < d ∧ (∀ y• Abs (y - t) < d ⇒ y ∈ A)))
lim_seq_open_ℝ_thm
⊢ ∀ s x
fill• s -> x
fill⇔ (∀ A
fill• A ∈ OpenR ∧ x ∈ A
fill⇒ (∃ n• ∀ m• n ≤ m ⇒ s m ∈ A))
cts_open_ℝ_thm
⊢ ∀ f
fill• (∀ x• f Cts x)
fill⇔ (∀ A• A ∈ OpenR ⇒ {x|f x ∈ A} ∈ OpenR)
closed_interval_closed_thm
⊢ ∀ x y• ClosedInterval x y ∈ ClosedR
cts_estimate_thm
⊢ ∀ f x lb ub
fill• f Cts x
fill∧ (∀ d
fill• 0. < d
fill⇒ (∃ z• Abs (z - x) < d ∧ lb ≤ f z)
fill∧ (∃ z• Abs (z - x) < d ∧ f z ≤ ub))
fill⇒ lb ≤ f x ∧ f x ≤ ub
cts_estimate_0_thm
⊢ ∀ f x
fill• f Cts x
fill∧ (∀ d
fill• 0. < d
fill⇒ (∃ z• Abs (z - x) < d ∧ 0. ≤ f z)
fill∧ (∃ z• Abs (z - x) < d ∧ f z ≤ 0.))
fill⇒ f x = 0.
cts_limit_unique_thm
⊢ ∀ f g x a b
fill• a < x
fill∧ x < b
fill∧ f Cts x
fill∧ g Cts x
fill∧ (∀ y• a < y ∧ y < b ∧ ¬ y = x ⇒ f y = g y)
fill⇒ f x = g x
cts_open_interval_thm
⊢ ∀ f a b x
fill• f x ∈ OpenInterval a b
fill∧ (∀ c d
fill• f x ∈ OpenInterval c d
fill∧ ClosedInterval c d ⊆ OpenInterval a b
fill⇒ (∃ s t
fill• x ∈ OpenInterval s t
fill∧ (∀ y
fill• y ∈ OpenInterval s t
fill⇒ f y ∈ OpenInterval c d)))
fill⇒ f Cts x
darboux_cts_mono_thm
⊢ ∀ f a b x
fill• (∀ x y
fill• x ∈ ClosedInterval a b
fill∧ y ∈ ClosedInterval a b
fill∧ x < y
fill⇒ f x < f y)
fill∧ (∀ y
fill• y ∈ OpenInterval (f a) (f b)
fill⇒ (∃ x• a < x ∧ x < b ∧ f x = y))
fill∧ x ∈ OpenInterval a b
fill⇒ f Cts x
darboux_cts_mono_thm1
⊢ ∀ f a b x
fill• (∀ x y
fill• x ∈ OpenInterval a b
fill∧ y ∈ OpenInterval a b
fill∧ x < y
fill⇒ f x < f y)
fill∧ (∀ x y z
fill• x ∈ OpenInterval a b
fill∧ y ∈ OpenInterval a b
fill∧ z ∈ OpenInterval (f x) (f y)
fill⇒ (∃ t• t ∈ OpenInterval a b ∧ f t = z))
fill∧ x ∈ OpenInterval a b
fill⇒ f Cts x
caratheodory_deriv_thm
⊢ ∀ f c x
fill• (f Deriv c) x
fill⇔ (∃ g
fill• (∀ y• f y - f x = g y * (y - x))
fill∧ g Cts x
fill∧ g x = c)
deriv_cts_thm
⊢ ∀ f c x• (f Deriv c) x ⇒ f Cts x
const_deriv_thm
⊢ ∀ c t• ((λ x• c) Deriv 0.) t
id_deriv_thm
⊢ ∀ t• ((λ x• x) Deriv 1.) t
plus_deriv_thm
⊢ ∀ f1 c1 x f2 c2
fill• (f1 Deriv c1) x ∧ (f2 Deriv c2) x
fill⇒ ((λ y• f1 y + f2 y) Deriv c1 + c2) x
plus_const_deriv_thm
⊢ ∀ c x• ($+ c Deriv 1.) x
times_deriv_thm
⊢ ∀ f1 c1 x f2 c2
fill• (f1 Deriv c1) x ∧ (f2 Deriv c2) x
fill⇒ ((λ y• f1 y * f2 y)
fillDeriv c1 * f2 x + f1 x * c2)
fillx
times_const_deriv_thm
⊢ ∀ c x• ($* c Deriv c) x
comp_deriv_thm
⊢ ∀ f1 c1 f2 c2 x
fill• (f1 Deriv c1) (f2 x) ∧ (f2 Deriv c2) x
fill⇒ ((λ y• f1 (f2 y)) Deriv c1 * c2) x
minus_deriv_thm
⊢ ∀ c t• (~ Deriv ~ 1.) t
minus_comp_deriv_thm
⊢ ∀ f c t• (f Deriv c) t ⇒ ((λ x• ~ (f x)) Deriv ~ c) t
ℝ_ℕ_exp_deriv_thm
⊢ ∀ n t
fill• ((λ x• x ^ (n + 1)) Deriv (ℕℝ n + 1.) * t ^ n) t
recip_deriv_thm
⊢ ∀ t• ¬ t = 0. ⇒ ($-1 Deriv ~ (t -1 * t -1)) t
recip_comp_deriv_thm
⊢ ∀ f c t
fill• (f Deriv c) t ∧ ¬ f t = 0.
fill⇒ ((λ x• f x -1)
fillDeriv ~ (f t -1 * f t -1) * c)
fillt
poly_deriv_thm
⊢ ∀ l x
fill• (PolyEval l Deriv PolyEval (DerivCoeffs l) x) x
deriv_local_thm
⊢ ∀ f g x a b c
fill• a < x
fill∧ x < b
fill∧ (∀ y• a < y ∧ y < b ⇒ f y = g y)
fill∧ (g Deriv c) x
fill⇒ (f Deriv c) x
deriv_lim_fun_thm
⊢ ∀ f c x
fill• (f Deriv c) x
fill⇔ ((λ y• (f y - f x) / (y - x)) --> c) x
deriv_unique_thm
⊢ ∀ f x c d• (f Deriv c) x ∧ (f Deriv d) x ⇒ c = d
curtain_induction_thm
⊢ ∀ p
fill• (∃ x• p x)
fill∧ (∀ x• p x ⇒ (∀ y• y < x ⇒ p y))
fill∧ (∀ x• ∃ y z• y < x ∧ x < z ∧ (p y ⇒ p z))
fill⇒ (∀ x• p x)
bisection_thm
⊢ ∀ p a b
fill• (∀ x y z• x ≤ y ∧ y ≤ z ∧ p x y ∧ p y z ⇒ p x z)
fill∧ (∀ y
fill• ∃ d
fill• 0. < d
fill∧ (∀ x z
fill• x ≤ y ∧ y ≤ z ∧ z - x < d ⇒ p x z))
fill∧ a ≤ b
fill⇒ p a b
closed_interval_compact_thm
⊢ ∀ x y• ClosedInterval x y ∈ CompactR
finite_chain_thm
⊢ ∀ V
fill• V ∈ Finite
fill∧ ¬ V = {}
fill∧ (∀ A B• A ∈ V ∧ B ∈ V ⇒ A ⊆ B ∨ B ⊆ A)
fill⇒ (∃ A• A ∈ V ∧ ⋃ V = A)
cts_compact_maximum_thm
⊢ ∀ X f
fill• ¬ X = {} ∧ X ∈ CompactR ∧ (∀ x• f Cts x)
fill⇒ (∃ x• x ∈ X ∧ (∀ z• z ∈ X ⇒ f z ≤ f x))
cts_maximum_thm
⊢ ∀ f a b
fill• a ≤ b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill⇒ (∃ x
fill• a ≤ x
fill∧ x ≤ b
fill∧ (∀ z• a ≤ z ∧ z ≤ b ⇒ f z ≤ f x))
cts_abs_bounded_thm
⊢ ∀ f a b
fill• a ≤ b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill⇒ (∃ c• ∀ z• a ≤ z ∧ z ≤ b ⇒ Abs (f z) ≤ c)
intermediate_value_thm
⊢ ∀ f a b
fill• a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill⇒ (∀ y
fill• f a < y ∧ y < f b ∨ f b < y ∧ y < f a
fill⇒ (∃ x• a < x ∧ x < b ∧ f x = y))
local_min_thm
⊢ ∀ f x a b c
fill• a < x
fill∧ x < b
fill∧ (∀ y• a < y ∧ y < b ⇒ f x ≤ f y)
fill∧ (f Deriv c) x
fill⇒ c = 0.
local_max_thm
⊢ ∀ f x a b c
fill• a < x
fill∧ x < b
fill∧ (∀ y• a < y ∧ y < b ⇒ f y ≤ f x)
fill∧ (f Deriv c) x
fill⇒ c = 0.
rolle_thm
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill∧ f a = f b
fill⇒ (∃ x• a < x ∧ x < b ∧ (f Deriv 0.) x)
cauchy_mean_value_thm
⊢ ∀ f df g dg a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ g Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (g Deriv dg x) x)
fill⇒ (∃ x
fill• a < x
fill∧ x < b
fill∧ dg x * (f b - f a) = df x * (g b - g a))
mean_value_thm
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill⇒ (∃ x
fill• a < x ∧ x < b ∧ f b - f a = (b - a) * df x)
mean_value_thm1
⊢ ∀ f df a b
fill• a < b ∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ (f Deriv df x) x)
fill⇒ (∃ x
fill• a < x ∧ x < b ∧ f b - f a = (b - a) * df x)
deriv_0_thm1
⊢ ∀ f a b
fill• (∀ x• a < x ∧ x < b ⇒ (f Deriv 0.) x)
fill⇒ (∀ x y• a < x ∧ x < y ∧ y < b ⇒ f x = f y)
deriv_0_thm
⊢ ∀ f a b
fill• (∀ x• a < x ∧ x < b ⇒ (f Deriv 0.) x)
fill⇒ (∃ c• ∀ x• a < x ∧ x < b ⇒ f x = c)
deriv_0_thm2
⊢ ∀ f x y• (∀ x• (f Deriv 0.) x) ⇒ f x = f y
deriv_0_less_thm
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill∧ (∀ x• a < x ∧ x < b ⇒ 0. < df x)
fill⇒ f a < f b
deriv_linear_estimate_thm
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x ≤ b ⇒ (f Deriv df x) x)
fill∧ (∀ x• a < x ∧ x < b ⇒ Abs (df x) ≤ 1.)
fill⇒ Abs (f b - f a) ≤ b - a
ℝ_mono_inc_seq_thm
⊢ ∀ f
fill• (∀ m• f m ≤ f (m + 1)) ⇒ (∀ m n• f m ≤ f (m + n))
ℝ_mono_dec_seq_thm
⊢ ∀ f
fill• (∀ m• f (m + 1) ≤ f m) ⇒ (∀ m n• f (m + n) ≤ f m)
nested_interval_bounds_thm
⊢ ∀ L U
fill• (∀ m
fill• L m ≤ L (m + 1) ∧ U (m + 1) ≤ U m ∧ L m ≤ U m)
fill⇒ (∀ m n• L m ≤ U n)
nested_interval_diag_thm
⊢ ∀ X
fill• ∃ L U
fill• ∀ m
fill• L m ≤ L (m + 1)
fill∧ U (m + 1) ≤ U m
fill∧ L m < U m
fill∧ (X m < L m ∨ U m < X m)
nested_interval_intersection_thm
⊢ ∀ L U
fill• (∀ m
fill• L m ≤ L (m + 1) ∧ U (m + 1) ≤ U m ∧ L m ≤ U m)
fill⇒ (∃ x• ∀ m• L m ≤ x ∧ x ≤ U m)
ℝ_uncountable_thm
⊢ ∀ X• ∃ x• ∀ m• ¬ x = X m
∩_open_interval_thm
⊢ ∀ x1 y1 x2 y2
fill• ∃ x y
fill• OpenInterval x1 y1 ∩ OpenInterval x2 y2
fill= OpenInterval x y
∩_closed_interval_thm
⊢ ∀ x1 y1 x2 y2
fill• ∃ x y
fill• ClosedInterval x1 y1 ∩ ClosedInterval x2 y2
fill= ClosedInterval x y
⋃_open_ℝ_thm
⊢ ∀ V• V ⊆ OpenR ⇒ ⋃ V ∈ OpenR
∪_open_ℝ_thm
⊢ ∀ X Y• X ∈ OpenR ∧ Y ∈ OpenR ⇒ X ∪ Y ∈ OpenR
∩_open_ℝ_thm
⊢ ∀ X Y• X ∈ OpenR ∧ Y ∈ OpenR ⇒ X ∩ Y ∈ OpenR
⋂_closed_ℝ_thm
⊢ ∀ V• V ⊆ ClosedR ⇒ ⋂ V ∈ ClosedR
∩_closed_ℝ_thm
⊢ ∀ X Y• X ∈ ClosedR ∧ Y ∈ ClosedR ⇒ X ∩ Y ∈ ClosedR
∪_closed_ℝ_thm
⊢ ∀ X Y• X ∈ ClosedR ∧ Y ∈ ClosedR ⇒ X ∪ Y ∈ ClosedR
open_interval_open_thm
⊢ ∀ x y• OpenInterval x y ∈ OpenR
complement_open_interval_thm
⊢ ∀ x y• ~ (OpenInterval x y) = {t|t ≤ x} ∪ {t|y ≤ t}
complement_closed_interval_thm
⊢ ∀ x y• ~ (ClosedInterval x y) = {t|t < x} ∪ {t|y < t}
half_infinite_intervals_open_thm
⊢ ∀ x• {t|t < x} ∈ OpenR ∧ {t|x < t} ∈ OpenR
half_infinite_intervals_closed_thm
⊢ ∀ x• {t|t ≤ x} ∈ ClosedR ∧ {t|x ≤ t} ∈ ClosedR
empty_universe_open_closed_thm
⊢ {} ∈ OpenR
fill∧ Universe ∈ OpenR
fill∧ {} ∈ ClosedR
fill∧ Universe ∈ ClosedR
compact_closed_thm
⊢ CompactR ⊆ ClosedR
compact_min_max_thm
⊢ ∀ X
fill• ¬ X = {} ∧ X ∈ CompactR
fill⇒ (∃ L U
fill• L ∈ X ∧ U ∈ X ∧ (∀ x• x ∈ X ⇒ L ≤ x ∧ x ≤ U))
closed_⊆_compact_thm
⊢ ∀ X Y
fill• Y ∈ ClosedR ∧ Y ⊆ X ∧ X ∈ CompactR
fill⇒ Y ∈ CompactR
empty_universe_compact_thm
⊢ {} ∈ CompactR ∧ ¬ Universe ∈ CompactR
heine_borel_thm
⊢ ∀ X
fill• X ∈ CompactR
fill⇔ X ∈ ClosedR
fill∧ (∃ L U• ∀ x• x ∈ X ⇒ L ≤ x ∧ x ≤ U)
ℝ_connected_thm
⊢ ∀ X Y
fill• ¬ X = {}
fill∧ X ∈ OpenR
fill∧ ¬ Y = {}
fill∧ Y ∈ OpenR
fill∧ (∀ x• x ∈ X ∪ Y)
fill⇒ (∃ x• x ∈ X ∩ Y)
lim_seq_cauchy_seq_thm
⊢ ∀ s x
fill• s -> x
fill⇒ (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
fin_seq_bounded_thm
⊢ ∀ s n• ∃ b• ∀ m• m ≤ n ⇒ s m < b
cauchy_seq_bounded_above_thm
⊢ ∀ s
fill• (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
fill⇒ (∃ b• ∀ m• s m < b)
cauchy_seq_bounded_below_thm
⊢ ∀ s
fill• (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
fill⇒ (∃ b• ∀ m• b < s m)
lim_seq_mono_inc_sup_thm
⊢ ∀ s ub
fill• (∀ m• s m ≤ ub ∧ s m ≤ s (m + 1))
fill⇒ s -> Sup {t|∃ m• t = s m}
fill∧ (∀ m• s m ≤ Sup {t|∃ m• t = s m})
lim_seq_mono_inc_thm
⊢ ∀ s ub
fill• (∀ m• s m ≤ ub ∧ s m ≤ s (m + 1))
fill⇒ (∃ x• s -> x ∧ (∀ m• s m ≤ x))
lim_seq_mono_dec_thm
⊢ ∀ s lb
fill• (∀ m• lb ≤ s m ∧ s (m + 1) ≤ s m)
fill⇒ (∃ x• s -> x ∧ (∀ m• x ≤ s m))
lim_sup_thm
⊢ ∀ s lb ub
fill• (∀ m• lb ≤ s m ∧ s m ≤ ub)
fill⇒ (∃ lim_sup
fill• ∀ e
fill• 0. < e
fill⇒ (∃ n• ∀ m• n ≤ m ⇒ s m < lim_sup + e)
fill∧ (∀ n• ∃ m• n ≤ m ∧ lim_sup < s m + e))
lim_inf_thm
⊢ ∀ s lb ub
fill• (∀ m• lb ≤ s m ∧ s m ≤ ub)
fill⇒ (∃ lim_inf
fill• ∀ e
fill• 0. < e
fill⇒ (∃ n• ∀ m• n ≤ m ⇒ lim_inf - e < s m)
fill∧ (∀ n• ∃ m• n ≤ m ∧ s m - e < lim_inf))
cauchy_seq_lim_seq_thm
⊢ ∀ s
fill• (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
fill⇒ (∃ x• s -> x)
lim_seq_⇔_cauchy_seq_thm
⊢ ∀ s
fill• (∃ x• s -> x)
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m ⇒ Abs (s k - s m) < e))
lim_fun_lim_seq_thm
⊢ ∀ f c x
fill• (f --> c) x
fill⇔ (∀ s
fill• s -> x ∧ (∀ m• ¬ s m = x)
fill⇒ (λ m• f (s m)) -> c)
const_lim_fun_thm
⊢ ∀ c t• ((λ x• c) --> c) t
id_lim_fun_thm
⊢ ∀ t• ((λ x• x) --> t) t
plus_lim_fun_thm
⊢ ∀ f1 t1 x f2 t2
fill• (f1 --> t1) x ∧ (f2 --> t2) x
fill⇒ ((λ x• f1 x + f2 x) --> t1 + t2) x
times_lim_fun_thm
⊢ ∀ f1 t1 x f2 t2
fill• (f1 --> t1) x ∧ (f2 --> t2) x
fill⇒ ((λ x• f1 x * f2 x) --> t1 * t2) x
recip_lim_fun_thm
⊢ ∀ f t x
fill• (f --> t) x ∧ ¬ t = 0.
fill⇒ ((λ x• f x -1) --> t -1) x
comp_lim_fun_thm
⊢ ∀ f t x g
fill• (f --> t) x ∧ g Cts t ⇒ ((λ x• g (f x)) --> g t) x
cts_lim_fun_thm
⊢ ∀ f x• f Cts x ⇒ (f --> f x) x
comp_lim_fun_thm1
⊢ ∀ f t x g
fill• (g --> t) (f x)
fill∧ f Cts x
fill∧ (∀ y• f y = f x ⇔ y = x)
fill⇒ ((λ x• g (f x)) --> t) x
poly_lim_fun_thm
⊢ ∀ f x• f ∈ PolyFunc ⇒ (f --> f x) x
lim_fun_upper_bound_thm
⊢ ∀ u d c t x
fill• 0. < d
fill∧ (∀ y• Abs (y - x) < d ∧ ¬ y = x ⇒ u y ≤ c)
fill∧ (u --> t) x
fill⇒ t ≤ c
lim_fun_unique_thm
⊢ ∀ u s t x• (u --> s) x ∧ (u --> t) x ⇒ s = t
lim_fun_local_thm
⊢ ∀ u v s t x a b
fill• (u --> s) x
fill∧ a < x
fill∧ x < b
fill∧ (∀ t• a < t ∧ t < b ∧ ¬ t = x ⇒ u t = v t)
fill⇒ (v --> s) x
deriv_lim_fun_thm1
⊢ ∀ f c x
fill• (f Deriv c) x
fill⇔ ((λ y• (f y - f x) * (y - x) -1) --> c) x
comp_lim_fun_thm2
⊢ ∀ f a b t x g
fill• x ∈ OpenInterval a b
fill∧ (g --> t) (f x)
fill∧ f Cts x
fill∧ (∀ y
fill• y ∈ OpenInterval a b ⇒ (f y = f x ⇔ y = x))
fill⇒ ((λ x• g (f x)) --> t) x
inverse_deriv_thm
⊢ ∀ f g a b x c
fill• x ∈ OpenInterval a b
fill∧ (∀ y• y ∈ OpenInterval a b ⇒ f (g y) = y)
fill∧ (f Deriv c) (g x)
fill∧ g Cts x
fill∧ ¬ c = 0.
fill⇒ (g Deriv c -1) x
const_unif_lim_seq_thm
⊢ ∀ h X• ((λ m• h) ---> h) X
plus_unif_lim_seq_thm
⊢ ∀ u1 h1 X u2 h2
fill• (u1 ---> h1) X ∧ (u2 ---> h2) X
fill⇒ ((λ m y• u1 m y + u2 m y)
fill---> (λ y• h1 y + h2 y))
fillX
bounded_unif_limit_thm
⊢ ∀ u g X c
fill• (u ---> g) X ∧ (∀ y m• y ∈ X ⇒ Abs (u m y) < c)
fill⇒ (∃ d• ∀ y• y ∈ X ⇒ Abs (g y) < d)
times_unif_lim_seq_thm
⊢ ∀ u g v h X c d
fill• (u ---> g) X
fill∧ (v ---> h) X
fill∧ (∀ y m• y ∈ X ⇒ Abs (u m y) < c)
fill∧ (∀ y m• y ∈ X ⇒ Abs (v m y) < d)
fill⇒ ((λ m y• u m y * v m y) ---> (λ y• g y * h y))
fillX
unif_lim_seq_bounded_thm
⊢ ∀ u h a b
fill• a < b
fill∧ (u ---> h) (ClosedInterval a b)
fill∧ (∀ y• a ≤ y ∧ y ≤ b ⇒ h Cts y)
fill⇒ (∃ c n
fill• ∀ m y• n ≤ m ∧ a ≤ y ∧ y ≤ b ⇒ Abs (u m y) < c)
unif_lim_seq_⊆_thm
⊢ ∀ u h X Y• (u ---> h) X ∧ Y ⊆ X ⇒ (u ---> h) Y
unif_lim_seq_shift_thm
⊢ ∀ m u h X• (u ---> h) X ⇔ ((λ n• u (n + m)) ---> h) X
unif_lim_seq_cts_thm
⊢ ∀ u h x a b
fill• (u ---> h) (OpenInterval a b)
fill∧ a < x
fill∧ x < b
fill∧ (∀ m• u m Cts x)
fill⇒ h Cts x
unif_lim_seq_cauchy_seq_thm
⊢ ∀ u f X
fill• (u ---> f) X
fill⇒ (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m
fill⇒ (∀ y
fill• y ∈ X ⇒ Abs (u k y - u m y) < e)))
cauchy_seq_unif_lim_seq_thm
⊢ ∀ u X
fill• (∀ e
fill• 0. < e
fill⇒ (∃ n
fill• ∀ k m
fill• n ≤ k ∧ n ≤ m
fill⇒ (∀ y
fill• y ∈ X ⇒ Abs (u k y - u m y) < e)))
fill⇒ (∃ f• (u ---> f) X)
unif_lim_seq_pointwise_lim_seq_thm
⊢ ∀ u f X x• (u ---> f) X ∧ x ∈ X ⇒ (λ m• u m x) -> f x
unif_lim_seq_pointwise_unique_thm
⊢ ∀ u f g X x c
fill• (u ---> f) X ∧ x ∈ X ∧ (λ m• u m x) -> c ⇒ f x = c
unif_lim_seq_unique_thm
⊢ ∀ u f g X x
fill• (u ---> f) X ∧ (u ---> g) X ∧ x ∈ X ⇒ f x = g x
lim_fun_lim_seq_interchange_thm
⊢ ∀ u f a b x s
fill• (u ---> f) (OpenInterval a b \ {x})
fill∧ a < x
fill∧ x < b
fill∧ (∀ m• (u m --> s m) x)
fill⇒ (∃ c• (f --> c) x ∧ s -> c)
unif_lim_seq_deriv_estimate_thm
⊢ ∀ du df x0 y0 A B u e
fill• (du ---> df) (OpenInterval A B)
fill∧ (∀ y m• A < y ∧ y < B ⇒ (u m Deriv du m y) y)
fill∧ A < x0
fill∧ x0 < B
fill∧ (λ m• u m x0) -> y0
fill∧ 0. < e
fill⇒ (∃ N
fill• ∀ n m x t
fill• N ≤ n ∧ N ≤ m ∧ A < x ∧ x < B ∧ A < t ∧ t < B
fill⇒ Abs
fill(u n t + ~ (u m t) + ~ (u n x) + u m x)
fill≤ Abs (t + ~ x) * e)
unif_lim_seq_deriv_thm
⊢ ∀ u du df A B x0 y0
fill• (du ---> df) (OpenInterval A B)
fill∧ (∀ y m
fill• y ∈ OpenInterval A B ⇒ (u m Deriv du m y) y)
fill∧ x0 ∈ OpenInterval A B
fill∧ (λ m• u m x0) -> y0
fill⇒ (∃ f
fill• (u ---> f) (OpenInterval A B)
fill∧ (∀ y
fill• y ∈ OpenInterval A B ⇒ (f Deriv df y) y))
power_series_series_thm
⊢ ∀ s
fill• PowerSeries s
fill= (λ n x• Series (λ m• s m * x ^ m) n)
series_power_series_thm
⊢ ∀ s• Series s = (λ n• PowerSeries s n 1.)
power_series_0_arg_thm
⊢ (∀ s• PowerSeries s 0 0. = 0.)
fill∧ (∀ s m• PowerSeries s (m + 1) 0. = s 0)
power_series_limit_0_thm
⊢ ∀ s• (λ m• PowerSeries s m 0.) -> s 0
plus_series_thm
⊢ ∀ s1 s2
fill• Series (λ m• s1 m + s2 m)
fill= (λ n• Series s1 n + Series s2 n)
series_0_thm
⊢ Series (λ m• 0.) = (λ m• 0.)
const_times_series_thm
⊢ ∀ s c• Series (λ m• c * s m) = (λ n• c * Series s n)
lim_seq_ℕℝ_recip_eq_0_thm
⊢ (λ m• ℕℝ m -1) -> 0.
lim_seq_ℝ_ℕ_exp_eq_0_thm
⊢ ∀ x• ~ 1. < x ∧ x < 1. ⇒ (λ m• x ^ m) -> 0.
series_shift_thm
⊢ ∀ n s
fill• Series (λ m• s (m + n))
fill= (λ m• Series s (m + n) - Series s n)
lim_series_shift_thm
⊢ ∀ n s x
fill• Series s -> x
fill⇔ Series (λ m• s (m + n)) -> x - Series s n
lim_series_shift_∃_thm
⊢ ∀ n s
fill• (∃ x• Series s -> x)
fill⇔ (∃ x• Series (λ m• s (m + n)) -> x)
lim_series_bounded_thm
⊢ ∀ e s c
fill• 0. < e ∧ Series s -> c
fill⇒ (∃ m• ∀ n• m ≤ n ⇒ Abs (s n) < e)
geometric_sum_thm1
⊢ ∀ n x
fill• ¬ x = 1.
fill⇒ PolyEval ((λ m• 1.) To (n + 1)) x
fill= (1. - x ^ (n + 1)) / (1. - x)
geometric_sum_thm
⊢ ∀ n x
fill• ¬ x = 1.
fill⇒ Series (λ m• x ^ m) (n + 1)
fill= (1. - x ^ (n + 1)) / (1. - x)
geometric_series_thm
⊢ ∀ x
fill• ~ 1. < x ∧ x < 1.
fill⇒ (λ n• PowerSeries (λ m• 1.) n x)
fill-> 1. / (1. - x)
geometric_series_series_thm
⊢ ∀ x
fill• (λ n• PowerSeries (λ m• 1.) n x)
fill= Series (λ m• x ^ m)
geometric_series_thm1
⊢ ∀ x
fill• ~ 1. < x ∧ x < 1.
fill⇒ Series (λ m• x ^ m) -> 1. / (1. - x)
weierstrass_test_thm
⊢ ∀ u X s c
fill• (∀ m x• x ∈ X ⇒ Abs (u m x) ≤ s m) ∧ Series s -> c
fill⇒ (∃ f
fill• ((λ m x• Series (λ m• u m x) m) ---> f) X)
comparison_test_thm
⊢ ∀ s1 s2 c2
fill• (∀ m• Abs (s1 m) ≤ s2 m) ∧ Series s2 -> c2
fill⇒ (∃ c1• Series s1 -> c1)
simple_root_test_thm
⊢ ∀ s b m
fill• 0. < b ∧ b < 1. ∧ (∀ n• m ≤ n ⇒ Abs (s n) ≤ b ^ n)
fill⇒ (∃ c• Series s -> c)
root_test_thm
⊢ ∀ s b d m
fill• b < 1. ∧ (∀ n• m ≤ n ⇒ Abs (s n) ≤ d * b ^ n)
fill⇒ (∃ c• Series s -> c)
ratio_test_thm1
⊢ ∀ s b m
fill• (∀ m• ¬ s m = 0.)
fill∧ 0. < b
fill∧ b < 1.
fill∧ (∀ n• m ≤ n ⇒ Abs (s (n + 1) / s n) < b)
fill⇒ (∃ c• Series s -> c)
ratio_test_thm
⊢ ∀ s b
fill• (∀ m• ¬ s m = 0.)
fill∧ 0. ≤ b
fill∧ b < 1.
fill∧ (λ n• Abs (s (n + 1) / s n)) -> b
fill⇒ (∃ c• Series s -> c)
power_series_convergence_thm
⊢ ∀ s B C b
fill• 0. < B
fill∧ 0. < b
fill∧ b < B
fill∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C
fill⇒ (∃ f
fill• (PowerSeries s ---> f) (OpenInterval (~ b) b))
power_series_deriv_coeffs_thm
⊢ ∀ s n x
fill• (PowerSeries s (n + 1)
fillDeriv PowerSeries
fill(λ m• ℕℝ (m + 1) * s (m + 1))
filln
fillx)
fillx
power_series_deriv_lemma1
⊢ ∀ b
fill• 0. < b ∧ b < 1.
fill⇒ (∃ c• Series (λ m• ℕℝ (m + 1) * b ^ m) -> c)
power_series_deriv_lemma2
⊢ ∀ s C b
fill• 0. < b
fill∧ b < 1.
fill∧ (λ m• PowerSeries (λ m• Abs (s m)) m 1.) -> C
fill⇒ (∃ D
fill• (λ m
fill• PowerSeries
fill(λ m• Abs (ℕℝ (m + 1) * s (m + 1)))
fillm
fillb)
fill-> D)
power_series_scale_arg_thm
⊢ ∀ c s m y
fill• PowerSeries s m (c * y)
fill= PowerSeries (λ m• s m * c ^ m) m y
power_series_scale_coeffs_thm
⊢ ∀ c s m y
fill• PowerSeries (λ m• c * s m) m y
fill= c * PowerSeries s m y
power_series_deriv_lim_seq_convergence_thm
⊢ ∀ s B C b
fill• 0. < b
fill∧ b < B
fill∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C
fill⇒ (∃ D
fill• (λ m
fill• PowerSeries
fill(λ m• Abs (ℕℝ (m + 1) * s (m + 1)))
fillm
fillb)
fill-> D)
power_series_deriv_convergence_thm
⊢ ∀ s B C b
fill• 0. < B
fill∧ 0. < b
fill∧ b < B
fill∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C
fill⇒ (∃ df
fill• (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1))
fill---> df)
fill(OpenInterval (~ b) b))
power_series_main_thm
⊢ ∀ s B C b
fill• 0. < b
fill∧ b < B
fill∧ (λ m• PowerSeries (λ m• Abs (s m)) m B) -> C
fill⇒ (∃ f df
fill• (PowerSeries s ---> f) (OpenInterval (~ b) b)
fill∧ (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1))
fill---> df)
fill(OpenInterval (~ b) b)
fill∧ (∀ y
fill• y ∈ OpenInterval (~ b) b
fill⇒ (f Deriv df y) y))
power_series_main_thm1
⊢ ∀ s b
fill• 0. < b
fill∧ (∀ x
fill• 0. < x
fill⇒ (∃ c
fill• (λ m• PowerSeries (λ m• Abs (s m)) m x)
fill-> c))
fill⇒ (∃ f df
fill• (PowerSeries s ---> f) (OpenInterval (~ b) b)
fill∧ (PowerSeries (λ m• ℕℝ (m + 1) * s (m + 1))
fill---> df)
fill(OpenInterval (~ b) b)
fill∧ (∀ y
fill• y ∈ OpenInterval (~ b) b
fill⇒ (f Deriv df y) y))
power_series_main_thm2
⊢ ∀ s
fill• (∀ x
fill• 0. < x
fill⇒ (∃ c
fill• (λ m• PowerSeries (λ m• Abs (s m)) m x)
fill-> c))
fill⇒ (∃ f df
fill• (∀ x• (λ m• PowerSeries s m x) -> f x)
fill∧ (∀ x
fill• (λ m
fill• PowerSeries
fill(λ m• ℕℝ (m + 1) * s (m + 1))
fillm
fillx)
fill-> df x)
fill∧ (∀ x• (f Deriv df x) x)
fill∧ f 0. = s 0)
power_series_main_thm3
⊢ ∀ s
fill• (∀ x
fill• 0. < x
fill⇒ (∃ c
fill• (λ m• PowerSeries (λ m• Abs (s m)) m x)
fill-> c))
fill⇒ (∃ f d1f d2f
fill• (∀ x• (λ m• PowerSeries s m x) -> f x)
fill∧ (∀ x
fill• (λ m
fill• PowerSeries
fill(λ m• ℕℝ (m + 1) * s (m + 1))
fillm
fillx)
fill-> d1f x)
fill∧ (∀ x
fill• (λ m
fill• PowerSeries
fill(λ m
fill• ℕℝ (m + 1)
fill* ℕℝ (m + 2)
fill* s (m + 2))
fillm
fillx)
fill-> d2f x)
fill∧ (∀ x• (f Deriv d1f x) x)
fill∧ (∀ x• (d1f Deriv d2f x) x)
fill∧ f 0. = s 0
fill∧ d1f 0. = s 1)
factorial_linear_estimate_thm
⊢ ∀ m• 1. ≤ ℕℝ (m !) ∧ ℕℝ m ≤ ℕℝ (m !)
factorial_0_less_thm
⊢ ∀ m• 0. < ℕℝ (m !)
factorial_times_recip_thm
⊢ ∀ m• ℕℝ (m + 1) * ℕℝ ((m + 1) !) -1 = ℕℝ (m !) -1
gen_rolle_thm
⊢ ∀ n D a b
fill• a < b
fill∧ (∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x)
fill∧ (∀ m x
fill• m ≤ n ∧ a < x ∧ x < b
fill⇒ (D m Deriv D (m + 1) x) x)
fill∧ (∀ m• m ≤ n ⇒ D m a = 0.)
fill∧ D 0 b = 0.
fill⇒ (∃ x• a < x ∧ x < b ∧ D (n + 1) x = 0.)
taylor_thm
⊢ ∀ n f D a b
fill• a < b
fill∧ D 0 = f
fill∧ (∀ m x• m ≤ n ∧ a ≤ x ∧ x ≤ b ⇒ D m Cts x)
fill∧ (∀ m x
fill• m ≤ n ∧ a < x ∧ x < b
fill⇒ (D m Deriv D (m + 1) x) x)
fill⇒ (∃ x
fill• a < x
fill∧ x < b
fill∧ f b
fill= PowerSeries
fill(λ m• D m a * ℕℝ (m !) -1)
fill(n + 1)
fill(b - a)
fill+ D (n + 1) x
fill* (b - a) ^ (n + 1)
fill* ℕℝ ((n + 1) !) -1)
exp_series_convergence_thm
⊢ ∀ x
fill• 0. < x
fill⇒ (∃ c
fill• (λ m
fill• PowerSeries (λ m• Abs (ℕℝ (m !) -1)) m x)
fill-> c)
exp_consistency_thm
⊢ ∃ f
fill• (∀ y• (f Deriv f y) y)
fill∧ f 0. = 1.
fill∧ (∀ x
fill• (λ m• PowerSeries (λ m• ℕℝ (m !) -1) m x)
fill-> f x)
Exp_consistent
⊢ Consistent
fill(λ Exp'
fill• Exp' 0. = 1. ∧ (∀ x• (Exp' Deriv Exp' x) x))
exp_def
⊢ Exp 0. = 1. ∧ (∀ x• (Exp Deriv Exp x) x)
exp_unique_thm
⊢ ∀ f g a b t
fill• (∀ x• x ∈ OpenInterval a b ⇒ ¬ f x = 0.)
fill∧ (∀ x• x ∈ OpenInterval a b ⇒ (f Deriv f x) x)
fill∧ (∀ x• x ∈ OpenInterval a b ⇒ (g Deriv g x) x)
fill∧ t ∈ OpenInterval a b
fill⇒ (∀ x
fill• x ∈ OpenInterval a b
fill⇒ g x = g t * f t -1 * f x)
exp_cts_thm
⊢ ∀ x• Exp Cts x
exp_¬_eq_0_thm
⊢ ∀ x• ¬ Exp x = 0.
exp_minus_thm
⊢ ∀ x• Exp (~ x) = Exp x -1
exp_0_less_thm
⊢ ∀ x• 0. < Exp x
exp_plus_thm
⊢ ∀ x y• Exp (x + y) = Exp x * Exp y
exp_clauses
⊢ Exp 0. = 1.
fill∧ (∀ x• Exp (~ x) = Exp x -1)
fill∧ (∀ x y• Exp (x + y) = Exp x * Exp y)
fill∧ (∀ x• 0. < Exp x)
fill∧ (∀ x• 0. ≤ Exp x)
exp_less_mono_thm
⊢ ∀ x y• x < y ⇔ Exp x < Exp y
exp_power_series_thm
⊢ ∀ x
fill• (λ m• PowerSeries (λ m• ℕℝ (m !) -1) m x)
fill-> Exp x
Log_consistent
⊢ Consistent (λ Log'• ∀ x• Log' (Exp x) = x)
log_def
⊢ ∀ x• Log (Exp x) = x
exp_one_one_thm
⊢ OneOne Exp
exp_ℝ_ℕ_exp_thm
⊢ ∀ m x• Exp (ℕℝ m * x) = Exp x ^ m
exp_0_less_onto_thm
⊢ ∀ x• 0. < x ⇒ (∃ y• x = Exp y)
exp_log_thm
⊢ ∀ x• 0. < x ⇒ Exp (Log x) = x
log_less_mono_thm
⊢ ∀ x y• 0. < x ∧ x < y ⇒ Log x < Log y
log_cts_thm
⊢ ∀ x• 0. < x ⇒ Log Cts x
log_deriv_thm
⊢ ∀ x• 0. < x ⇒ (Log Deriv x -1) x
log_clauses
⊢ Log 1. = 0.
fill∧ (∀ x• 0. < x ⇒ Log (x -1) = ~ (Log x))
fill∧ (∀ x y
fill• 0. < x ∧ 0. < y ⇒ Log (x * y) = Log x + Log y)
ℝ_ℕ_exp_exp_log_thm
⊢ ∀ m x• 0. < x ⇒ x ^ m = Exp (ℕℝ m * Log x)
positive_root_thm
⊢ ∀ m x• ¬ m = 0 ∧ 0. < x ⇒ (∃ y• 0. < y ∧ y ^ m = x)
square_root_thm
⊢ ∀ x• 0. < x ⇔ (∃ y• 0. < y ∧ y ^ 2 = x)
square_root_thm1
⊢ ∀ x• 0. ≤ x ⇔ (∃ y• 0. ≤ y ∧ y ^ 2 = x)
square_root_unique_thm
⊢ ∀ x y• x ^ 2 = y ^ 2 ⇔ x = y ∨ x = ~ y
square_square_root_mono_thm
⊢ ∀ x y• 0. < x ∧ 0. < y ⇒ (x ^ 2 < y ^ 2 ⇔ x < y)
sin_series_convergence_thm
⊢ ∀ x
fill• 0. < x
fill⇒ (∃ c
fill• (λ m
fill• PowerSeries
fill(λ m
fill• Abs
fill(if m Mod 2 = 0
fillthen 0.
fillelse
fill~ 1. ^ (m Div 2)
fill* ℕℝ (m !) -1))
fillm
fillx)
fill-> c)
even_odd_thm
⊢ ∀ m• ∃ n• m = 2 * n ∨ m = 2 * n + 1
mod_2_div_2_thm
⊢ ∀ n
fill• (2 * n) Mod 2 = 0
fill∧ (2 * n + 1) Mod 2 = 1
fill∧ (2 * n) Div 2 = n
fill∧ (2 * n + 1) Div 2 = n
mod_2_cases_thm
⊢ ∀ m• m Mod 2 = 0 ∨ m Mod 2 = 1
mod_2_0_ℝ_ℕ_exp_thm
⊢ ∀ m x• m Mod 2 = 0 ⇒ ~ x ^ m = x ^ m
mod_2_1_ℝ_ℕ_exp_thm
⊢ ∀ m x• m Mod 2 = 1 ⇒ ~ x ^ m = ~ (x ^ m)
power_series_even_thm
⊢ ∀ s n x
fill• (∀ m• m Mod 2 = 1 ⇒ s m = 0.)
fill⇒ PowerSeries s n (~ x) = PowerSeries s n x
power_series_odd_thm
⊢ ∀ s n x
fill• (∀ m• m Mod 2 = 0 ⇒ s m = 0.)
fill⇒ PowerSeries s n (~ x) = ~ (PowerSeries s n x)
sin_deriv_coeffs_thm
⊢ ∀ m
fill• ℕℝ (m + 1)
fill* ℕℝ (m + 2)
fill* (if (m + 2) Mod 2 = 0
fillthen 0.
fillelse
fill~ 1. ^ ((m + 2) Div 2)
fill* ℕℝ ((m + 2) !) -1)
fill= ~
fill(if m Mod 2 = 0
fillthen 0.
fillelse ~ 1. ^ (m Div 2) * ℕℝ (m !) -1)
sin_cos_consistency_thm
⊢ ∃ s c
fill• (∀ y• (s Deriv c y) y)
fill∧ (∀ y• (c Deriv ~ (s y)) y)
fill∧ s 0. = 0.
fill∧ c 0. = 1.
fill∧ (∀ x
fill• (λ n
fill• PowerSeries
fill(λ m
fill• if m Mod 2 = 0
fillthen 0.
fillelse
fill~ 1. ^ (m Div 2) * ℕℝ (m !) -1)
filln
fillx)
fill-> s x)
fill∧ (∀ x
fill• (λ n
fill• PowerSeries
fill(λ m
fill• ℕℝ (m + 1)
fill* (if (m + 1) Mod 2 = 0
fillthen 0.
fillelse
fill~ 1. ^ ((m + 1) Div 2)
fill* ℕℝ ((m + 1) !) -1))
filln
fillx)
fill-> c x)
Sin_consistent
Cos_consistent
⊢ Consistent
fill(λ (Sin', Cos')
fill• Sin' 0. = 0.
fill∧ Cos' 0. = 1.
fill∧ (∀ x• (Sin' Deriv Cos' x) x)
fill∧ (∀ x• (Cos' Deriv ~ (Sin' x)) x))
sin_def
cos_def
⊢ Sin 0. = 0.
fill∧ Cos 0. = 1.
fill∧ (∀ x• (Sin Deriv Cos x) x)
fill∧ (∀ x• (Cos Deriv ~ (Sin x)) x)
sin_cos_cts_thm
⊢ ∀ x• Sin Cts x ∧ Cos Cts x
cos_squared_plus_sin_squared_thm
⊢ ∀ x• Cos x ^ 2 + Sin x ^ 2 = 1.
sin_cos_unique_lemma1
⊢ ∀ f g x
fill• (∀ x• (f Deriv g x) x) ∧ (∀ x• (g Deriv ~ (f x)) x)
fill⇒ Cos x * g x + Sin x * f x = g 0.
fill∧ Cos x * f x - Sin x * g x = f 0.
sin_cos_unique_lemma2
⊢ ∀ f g x
fill• (∀ x• (f Deriv g x) x) ∧ (∀ x• (g Deriv ~ (f x)) x)
fill⇒ f x = f 0. * Cos x + g 0. * Sin x
fill∧ g x = g 0. * Cos x - f 0. * Sin x
sin_cos_unique_thm
⊢ ∀ f g x
fill• f 0. = 0.
fill∧ g 0. = 1.
fill∧ (∀ x• (f Deriv g x) x)
fill∧ (∀ x• (g Deriv ~ (f x)) x)
fill⇒ f x = Sin x ∧ g x = Cos x
sin_cos_power_series_thm
⊢ ∀ x
fill• (λ n
fill• PowerSeries
fill(λ m
fill• if m Mod 2 = 0
fillthen 0.
fillelse ~ 1. ^ (m Div 2) * ℕℝ (m !) -1)
filln
fillx)
fill-> Sin x
fill∧ (λ n
fill• PowerSeries
fill(λ m
fill• ℕℝ (m + 1)
fill* (if (m + 1) Mod 2 = 0
fillthen 0.
fillelse
fill~ 1. ^ ((m + 1) Div 2)
fill* ℕℝ ((m + 1) !) -1))
filln
fillx)
fill-> Cos x
sin_cos_plus_thm
⊢ ∀ x y
fill• Sin (x + y) = Sin x * Cos y + Cos x * Sin y
fill∧ Cos (x + y) = Cos x * Cos y - Sin x * Sin y
sin_cos_minus_thm
⊢ ∀ x• Sin (~ x) = ~ (Sin x) ∧ Cos (~ x) = Cos x
sin_0_group_thm
⊢ 0. ∈ {x|Sin x = 0.}
fill∧ (∀ x y
fill• x ∈ {x|Sin x = 0.} ∧ y ∈ {x|Sin x = 0.}
fill⇒ x + y ∈ {x|Sin x = 0.})
fill∧ (∀ x• x ∈ {x|Sin x = 0.} ⇒ ~ x ∈ {x|Sin x = 0.})
sin_0_ℕℝ_times_thm
⊢ ∀ x m• Sin x = 0. ⇒ Sin (ℕℝ m * x) = 0.
sin_eq_cos_sin_cos_twice_thm
⊢ ∀ x
fill• Sin x = Cos x
fill⇒ Sin (2. * x) = 1. ∧ Cos (2. * x) = 0.
sum_squares_abs_bound_thm
⊢ ∀ x y z• x ^ 2 + y ^ 2 = z ^ 2 ⇒ Abs x ≤ Abs z
sum_squares_abs_bound_thm1
⊢ ∀ x y• x ^ 2 + y ^ 2 = 1. ⇒ Abs x ≤ 1.
abs_sin_abs_cos_≤_1_thm
⊢ ∀ x• Abs (Sin x) ≤ 1. ∧ Abs (Cos x) ≤ 1.
cos_positive_estimate_thm
⊢ ∀ x• x ∈ OpenInterval 0. 1. ⇒ 0. < Cos x
sin_positive_estimate_thm
⊢ ∀ x• x ∈ OpenInterval 0. 2. ⇒ 0. < Sin x
cos_greater_root_2_thm
⊢ ∀ t
fill• 0. < t ∧ (∀ x• 0. < x ∧ x < t ⇒ 1 / 2 < Cos x ^ 2)
fill⇒ t ^ 2 ≤ 2.
cos_squared_eq_half_thm
⊢ ∀ e
fill• 0. < e
fill⇒ (∃ x
fill• 0. < x
fill∧ x ^ 2 < 2. + e
fill∧ 0. < Cos x
fill∧ Cos x ^ 2 = 1 / 2)
sin_eq_cos_exists_thm
⊢ ∃ x• x ∈ OpenInterval 0. 2. ∧ Sin x = Cos x
sin_positive_zero_thm
⊢ ∃ x• 0. < x ∧ Sin x = 0.
ℝ_discrete_subgroup_thm
⊢ ∀ G h a
fill• 0. ∈ G
fill∧ (∀ g h• g ∈ G ∧ h ∈ G ⇒ g + h ∈ G)
fill∧ (∀ g• g ∈ G ⇒ ~ g ∈ G)
fill∧ 0. < h
fill∧ h ∈ G
fill∧ 0. < a
fill∧ (∀ h• 0. < h ∧ h ∈ G ⇒ a < h)
fill⇒ (∃ g
fill• 0. < g
fill∧ g ∈ G
fill∧ (∀ h
fill• 0. < h ∧ h ∈ G ⇒ (∃ m• h = ℕℝ m * g)))
pi_consistency_thm
⊢ ∃ pi
fill• 0. < pi
fill∧ Sin pi = 0.
fill∧ (∀ x
fill• 0. < x ∧ Sin x = 0. ⇒ (∃ m• x = ℕℝ m * pi))
ArchimedesConstant_consistent
⊢ Consistent
fill(λ ArchimedesConstant'
fill• 0. < ArchimedesConstant'
fill∧ (∀ x
fill• Sin x = 0.
fill⇔ (∃ m• x = ℕℝ m * ArchimedesConstant')
fill∨ (∃ m
fill• x = ~ (ℕℝ m * ArchimedesConstant'))))
π_def
⊢ 0. < π
fill∧ (∀ x
fill• Sin x = 0.
fill⇔ (∃ m• x = ℕℝ m * π)
fill∨ (∃ m• x = ~ (ℕℝ m * π)))
ℕℝ_plus_1_times_bound_thm
⊢ (∀ c m• 0. < c ⇒ c ≤ ℕℝ (m + 1) * c)
fill∧ (∀ c m• c < 0. ⇒ ℕℝ (m + 1) * c ≤ c)
ℕℝ_0_less_¬_ℕℝ_times_π_thm
⊢ ∀ x m• 0. < x ⇒ ¬ x = ~ (ℕℝ m * π)
sin_¬_eq_0_thm
⊢ ∀ x• 0. < x ∧ x < π ⇒ ¬ Sin x = 0.
sin_0_π_0_less_thm
⊢ ∀ x• x ∈ OpenInterval 0. π ⇒ 0. < Sin x
sin_cos_π_over_2_thm
⊢ Sin (1 / 2 * π) = 1. ∧ Cos (1 / 2 * π) = 0.
sin_cos_plus_π_over_2_thm
⊢ ∀ x
fill• Sin (x + 1 / 2 * π) = Cos x
fill∧ Cos (x + 1 / 2 * π) = ~ (Sin x)
cos_¬_eq_0_thm
⊢ ∀ x• ~ (1 / 2) * π < x ∧ x < 1 / 2 * π ⇒ ¬ Cos x = 0.
cos_eq_0_thm
⊢ ∀ x
fill• Cos x = 0.
fill⇔ (∃ m• x = 1 / 2 * π + ℕℝ m * π)
fill∨ (∃ m• x = 1 / 2 * π - ℕℝ m * π)
sin_cos_plus_π_thm
⊢ ∀ x
fill• Sin (x + π) = ~ (Sin x) ∧ Cos (x + π) = ~ (Cos x)
sin_cos_π_thm
⊢ Sin π = 0. ∧ Cos π = ~ 1.
sin_cos_plus_2_π_thm
⊢ ∀ x
fill• Sin (x + 2. * π) = Sin x ∧ Cos (x + 2. * π) = Cos x
sin_cos_2_π_thm
⊢ Sin (2. * π) = 0. ∧ Cos (2. * π) = 1.
sin_cos_plus_even_times_π_thm
⊢ ∀ x m
fill• Sin (x + ℕℝ (2 * m) * π) = Sin x
fill∧ Cos (x + ℕℝ (2 * m) * π) = Cos x
sin_cos_even_times_π_thm
⊢ ∀ m
fill• Sin (ℕℝ (2 * m) * π) = 0.
fill∧ Cos (ℕℝ (2 * m) * π) = 1.
sin_cos_period_thm
⊢ ∀ x y
fill• x < y
fill⇒ (Sin x = Sin y ∧ Cos x = Cos y
fill⇔ (∃ m• y = x + ℕℝ (2 * m) * π))
sin_cos_onto_unit_circle_thm
⊢ ∀ x y
fill• x ^ 2 + y ^ 2 = 1.
fill⇒ (∃ z
fill• 0. ≤ z ∧ z < 2. * π ∧ x = Cos z ∧ y = Sin z)
sin_cos_onto_unit_circle_thm1
⊢ ∀ x y
fill• x ^ 2 + y ^ 2 = 1.
fill⇒ (∃1 z
fill• 0. ≤ z ∧ z < 2. * π ∧ x = Cos z ∧ y = Sin z)
lim_right_lim_seq_thm
⊢ ∀ f c x
fill• (f +#-> c) x
fill⇔ (∀ s
fill• s -> x ∧ (∀ m• x < s m) ⇒ (λ m• f (s m)) -> c)
lim_fun_lim_right_thm
⊢ ∀ f c x
fill• (f --> c) x
fill⇔ (f +#-> c) x ∧ ((λ y• f (~ y)) +#-> c) (~ x)
const_lim_right_thm
⊢ ∀ c x• ((λ x• c) +#-> c) x
id_lim_right_thm
⊢ ∀ x• ((λ x• x) +#-> x) x
plus_lim_right_thm
⊢ ∀ f1 c1 f2 c2 x
fill• (f1 +#-> c1) x ∧ (f2 +#-> c2) x
fill⇒ ((λ x• f1 x + f2 x) +#-> c1 + c2) x
times_lim_right_thm
⊢ ∀ f1 c1 f2 c2 x
fill• (f1 +#-> c1) x ∧ (f2 +#-> c2) x
fill⇒ ((λ x• f1 x * f2 x) +#-> c1 * c2) x
poly_lim_right_thm
⊢ ∀ f g c x
fill• f ∈ PolyFunc ∧ (g +#-> c) x
fill⇒ ((λ x• f (g x)) +#-> f c) x
recip_lim_right_thm
⊢ ∀ f c x
fill• (f +#-> c) x ∧ ¬ c = 0.
fill⇒ ((λ x• f x -1) +#-> c -1) x
lim_right_unique_thm
⊢ ∀ f c d x• (f +#-> c) x ∧ (f +#-> d) x ⇒ c = d
cts_lim_right_thm
⊢ ∀ f c x• f Cts x ∧ (f +#-> c) x ⇒ f x = c
lim_infinity_lim_seq_thm
⊢ ∀ f c
fill• f -+#> c
fill⇔ (∀ s• (∀ m• ℕℝ m ≤ s m) ⇒ (λ m• f (s m)) -> c)
lim_infinity_lim_right_thm
⊢ ∀ f c• f -+#> c ⇔ ((λ x• f (x -1)) +#-> c) 0.
lim_right_lim_infinity_thm
⊢ ∀ f c• ((λ x• f (x -1)) +#-> c) 0. ⇔ f -+#> c
const_lim_infinity_thm
⊢ ∀ c• (λ x• c) -+#> c
id_lim_infinity_thm
⊢ ∀ c• ¬ (λ x• x) -+#> c
plus_lim_infinity_thm
⊢ ∀ f1 c1 f2 c2
fill• f1 -+#> c1 ∧ f2 -+#> c2
fill⇒ (λ x• f1 x + f2 x) -+#> c1 + c2
times_lim_infinity_thm
⊢ ∀ f1 c1 f2 c2
fill• f1 -+#> c1 ∧ f2 -+#> c2
fill⇒ (λ x• f1 x * f2 x) -+#> c1 * c2
poly_lim_infinity_thm
⊢ ∀ f g c
fill• f ∈ PolyFunc ∧ g -+#> c ⇒ (λ x• f (g x)) -+#> f c
recip_lim_infinity_thm
⊢ ∀ f c
fill• f -+#> c ∧ ¬ c = 0. ⇒ (λ x• f x -1) -+#> c -1
recip_lim_infinity_0_thm
⊢ (λ x• x -1) -+#> 0.
lim_infinity_unique_thm
⊢ ∀ f c d• f -+#> c ∧ f -+#> d ⇒ c = d
div_infinity_pos_thm
⊢ ∀ f
fill• f -+#>+# ⇒ (∃ b• 0. < b ∧ (∀ x• b < x ⇒ 0. < f x))
const_plus_div_infinity_thm
⊢ ∀ f c• f -+#>+# ⇒ (λ x• c + f x) -+#>+#
id_div_infinity_thm
⊢ (λ x• x) -+#>+#
plus_div_infinity_thm
⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f x + g x) -+#>+#
const_times_div_infinity_thm
⊢ ∀ f c• f -+#>+# ∧ 0. < c ⇒ (λ x• c * f x) -+#>+#
times_div_infinity_thm
⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f x * g x) -+#>+#
power_div_infinity_thm
⊢ ∀ m• (λ x• x ^ (m + 1)) -+#>+#
less_div_infinity_thm
⊢ ∀ f g a
fill• f -+#>+# ∧ (∀ x• a < x ⇒ f x < g x) ⇒ g -+#>+#
bounded_deriv_div_infinity_thm
⊢ ∀ f df a c
fill• 0. < c
fill∧ (∀ x• a ≤ x ⇒ (f Deriv df x) x)
fill∧ (∀ x• a ≤ x ⇒ c < df x)
fill⇒ f -+#>+#
exp_div_infinity_thm
⊢ Exp -+#>+#
log_div_infinity_thm
⊢ Log -+#>+#
div_infinity_times_recip_thm
⊢ ∀ f a e
fill• f -+#>+# ∧ 0. < a ∧ 0. < e
fill⇒ (∃ b• ∀ x• b < x ⇒ a * f x -1 < e)
div_infinity_lim_right_thm
⊢ ∀ f
fill• f -+#>+#
fill⇔ ((λ x• f (x -1) -1) +#-> 0.) 0.
fill∧ (∃ b• ∀ x• b < x ⇒ 0. < f x)
div_infinity_lim_infinity_thm
⊢ ∀ f
fill• f -+#>+#
fill⇔ (λ x• f x -1) -+#> 0.
fill∧ (∃ b• ∀ x• b < x ⇒ 0. < f x)
comp_div_infinity_thm
⊢ ∀ f g• f -+#>+# ∧ g -+#>+# ⇒ (λ x• f (g x)) -+#>+#
rolle_thm1
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x < b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill∧ (∀ x• a < x ∧ x < b ⇒ ¬ df x = 0.)
fill⇒ (∀ x• a < x ∧ x < b ⇒ ¬ f x = f a)
l'hopital_lim_right_thm
⊢ ∀ f df g dg a b c
fill• a < b
fill∧ f a = 0.
fill∧ g a = 0.
fill∧ (∀ x• a ≤ x ∧ x < b ⇒ f Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (f Deriv df x) x)
fill∧ (∀ x• a ≤ x ∧ x < b ⇒ g Cts x)
fill∧ (∀ x• a < x ∧ x < b ⇒ (g Deriv dg x) x)
fill∧ (∀ x• a < x ∧ x < b ⇒ ¬ dg x = 0.)
fill∧ ((λ x• df x * dg x -1) +#-> c) a
fill⇒ ((λ x• f x * g x -1) +#-> c) a
cts_comp_minus_thm
⊢ ∀ f x• (λ x• f (~ x)) Cts x ⇔ f Cts ~ x
deriv_comp_minus_thm
⊢ ∀ f df x
fill• ((λ x• f (~ x)) Deriv ~ (df (~ x))) x
fill⇔ (f Deriv df (~ x)) (~ x)
l'hopital_lim_fun_thm
⊢ ∀ f df g dg a b c x
fill• a < x
fill∧ x < b
fill∧ f x = 0.
fill∧ g x = 0.
fill∧ (∀ y• a < y ∧ y < b ⇒ f Cts y)
fill∧ (∀ y
fill• a < y ∧ y < b ∧ ¬ y = x ⇒ (f Deriv df y) y)
fill∧ (∀ y• a < y ∧ y < b ⇒ g Cts y)
fill∧ (∀ y
fill• a < y ∧ y < b ∧ ¬ y = x ⇒ (g Deriv dg y) y)
fill∧ (∀ y• a < y ∧ y < b ⇒ ¬ dg y = 0.)
fill∧ ((λ y• df y * dg y -1) --> c) x
fill⇒ ((λ y• f y * g y -1) --> c) x
l'hopital_lim_infinity_thm
⊢ ∀ f df g dg a c
fill• g -+#>+#
fill∧ (∀ x• a < x ⇒ (f Deriv df x) x)
fill∧ (∀ x• a < x ⇒ (g Deriv dg x) x)
fill∧ (∀ x• a < x ⇒ ¬ dg x = 0.)
fill∧ (λ x• df x * dg x -1) -+#> c
fill⇒ (λ x• f x * g x -1) -+#> c
cts_deriv_deriv_thm
⊢ ∀ f df a b t
fill• (∀ x
fill• x ∈ OpenInterval a b \ {t}
fill⇒ (f Deriv df x) x)
fill∧ (∀ x• x ∈ OpenInterval a b ⇒ df Cts x)
fill∧ f Cts t
fill∧ t ∈ OpenInterval a b
fill⇒ (∀ x• x ∈ OpenInterval a b ⇒ (f Deriv df x) x)
lim_fun_id_over_sin_thm
⊢ ((λ x• x * Sin x -1) --> 1.) 0.
lim_infinity_recip_exp_thm
⊢ (λ x• Exp x -1) -+#> 0.
lim_infinity_id_over_exp_thm
⊢ (λ x• x * Exp x -1) -+#> 0.
lim_fun_power_over_exp_thm
⊢ ∀ m• (λ x• x ^ m * Exp x -1) -+#> 0.
lim_infinity_log_over_id_thm
⊢ (λ x• Log x * x -1) -+#> 0.
lim_fun_log_over_id_minus_1_thm
⊢ ((λ x• Log x * (x - 1.) -1) --> 1.) 1.
lim_fun_log_1_plus_over_id_thm
⊢ ((λ x• Log (1. + x) * x -1) --> 1.) 0.
lim_fun_e_thm
⊢ ((λ x• Exp (x -1 * Log (1. + x))) --> Exp 1.) 0.
lim_seq_e_thm
⊢ (λ m• (1. + ℕℝ m -1) ^ m) -> Exp 1.
ℝ_less_mono_⇔_thm
⊢ ∀ f
fill• (∀ x y• x < y ⇒ f x < f y)
fill⇔ (∀ x y• f x < f y ⇔ x < y)
ℝ_less_mono_⇔_≤_thm
⊢ ∀ f
fill• (∀ x y• x < y ⇒ f x < f y)
fill⇔ (∀ x y• f x ≤ f y ⇔ x ≤ y)
ℝ_less_mono_one_one_thm
⊢ ∀ f
fill• (∀ x y• x < y ⇒ f x < f y)
fill⇒ (∀ x y• f x = f y ⇔ x = y)
total_inverse_cts_thm
⊢ ∀ f g x
fill• (∀ x y• x < y ⇒ f x < f y)
fill∧ (∀ x• g (f x) = x)
fill∧ (∀ y• f (g y) = y)
fill⇒ g Cts f x
total_inverse_thm
⊢ ∀ f
fill• (∀ x y• x < y ⇒ f x < f y) ∧ (∀ y• ∃ x• f x = y)
fill⇒ (∃ g
fill• (∀ x• g (f x) = x)
fill∧ (∀ y• f (g y) = y)
fill∧ (∀ y• g Cts y)
fill∧ (∀ x y• x < y ⇒ g x < g y))
closed_half_infinite_inverse_thm1
⊢ ∀ f a
fill• (∀ x• a ≤ x ⇒ f Cts x)
fill∧ (∀ x y• a ≤ x ∧ x < y ⇒ f x < f y)
fill∧ (∀ y• f a ≤ y ⇒ (∃ x• a ≤ x ∧ f x = y))
fill⇒ (∃ g
fill• (∀ x• a ≤ x ⇒ g (f x) = x)
fill∧ (∀ y• f a ≤ y ⇒ f (g y) = y)
fill∧ (∀ y• g Cts y)
fill∧ (∀ x y• x < y ⇒ g x < g y))
closed_half_infinite_inverse_thm
⊢ ∀ f df a
fill• (∀ x• a ≤ x ⇒ f Cts x)
fill∧ (∀ x• a < x ⇒ (f Deriv df x) x)
fill∧ (∀ x• a < x ⇒ 0. < df x)
fill∧ (∀ y• f a ≤ y ⇒ (∃ x• a ≤ x ∧ f x = y))
fill⇒ (∃ g
fill• (∀ x• a ≤ x ⇒ g (f x) = x)
fill∧ (∀ y• f a ≤ y ⇒ f (g y) = y)
fill∧ (∀ y• g Cts y)
fill∧ (∀ x y• x < y ⇒ g x < g y))
cond_cts_thm
⊢ ∀ f g y
fill• f Cts y ∧ g Cts y ∧ f y = g y
fill⇒ (λ z• if z ≤ y then f z else g z) Cts y
cond_cts_thm1
⊢ ∀ f g a b y x
fill• (∀ x• x ∈ ClosedInterval a y ⇒ f Cts x)
fill∧ (∀ x• x ∈ ClosedInterval y b ⇒ g Cts x)
fill∧ f y = g y
fill∧ x ∈ ClosedInterval a b
fill⇒ (λ z• if z ≤ y then f z else g z) Cts x
closed_interval_inverse_thm
⊢ ∀ f df a b
fill• a < b
fill∧ (∀ x• x ∈ ClosedInterval a b ⇒ f Cts x)
fill∧ (∀ x
fill• x ∈ OpenInterval a b ⇒ (f Deriv df x) x)
fill∧ (∀ x• x ∈ OpenInterval a b ⇒ 0. < df x)
fill⇒ (∃ g
fill• (∀ x• x ∈ ClosedInterval a b ⇒ g (f x) = x)
fill∧ (∀ y
fill• y ∈ ClosedInterval (f a) (f b)
fill⇒ f (g y) = y)
fill∧ (∀ y• g Cts y)
fill∧ (∀ x y• x < y ⇒ g x < g y))
Sqrt_consistent
⊢ Consistent
fill(λ Sqrt'
fill• ∀ x
fill• 0. ≤ x
fill⇒ 0. ≤ Sqrt' x
fill∧ Sqrt' x ^ 2 = x
fill∧ Sqrt' Cts x)
sqrt_def
⊢ ∀ x
fill• 0. ≤ x ⇒ 0. ≤ Sqrt x ∧ Sqrt x ^ 2 = x ∧ Sqrt Cts x
sqrt_thm
⊢ ∀ x• 0. ≤ x ⇒ Sqrt x ^ 2 = x
sqrt_0_≤_thm
⊢ ∀ x• 0. ≤ x ⇒ 0. ≤ Sqrt x
sqrt_cts_thm
⊢ ∀ x• 0. ≤ x ⇒ Sqrt Cts x
sqrt_square_thm
⊢ ∀ x• Sqrt (x ^ 2) = Abs x
square_sqrt_thm
⊢ ∀ x y• x = y ^ 2 ⇒ Sqrt x = Abs y
sqrt_0_1_thm
⊢ Sqrt 0. = 0. ∧ Sqrt 1. = 1.
square_times_thm
⊢ ∀ x y• (x * y) ^ 2 = x ^ 2 * y ^ 2
sqrt_times_thm
⊢ ∀ x y
fill• 0. ≤ x ∧ 0. ≤ y ⇒ Sqrt (x * y) = Sqrt x * Sqrt y
square_recip_thm
⊢ ∀ x• ¬ x = 0. ⇒ (x -1) ^ 2 = (x ^ 2) -1
sqrt_pos_thm
⊢ ∀ x• 0. < x ⇒ 0. < Sqrt x
sqrt_recip_thm
⊢ ∀ x• 0. < x ⇒ Sqrt (x -1) = Sqrt x -1
sqrt_exp_log_thm
⊢ ∀ x• 0. < x ⇒ Sqrt x = Exp (1 / 2 * Log x)
sqrt_deriv_thm
⊢ ∀ x• 0. < x ⇒ (Sqrt Deriv 1 / 2 * Sqrt x * x -1) x
sqrt_mono_thm
⊢ ∀ x y• 0. ≤ x ∧ x < y ⇒ Sqrt x < Sqrt y
square_mono_≤_thm
⊢ ∀ x y• 0. ≤ x ∧ 0. ≤ y ⇒ (x ≤ y ⇔ x ^ 2 ≤ y ^ 2)
id_over_sqrt_thm
⊢ ∀ x• 0. < x ⇒ x * Sqrt x -1 = Sqrt x
sqrt_1_minus_sin_squared_thm
⊢ ∀ x• Sqrt (1. - Sin x ^ 2) = Abs (Cos x)
sqrt_1_minus_cos_squared_thm
⊢ ∀ x• Sqrt (1. - Cos x ^ 2) = Abs (Sin x)
tan_deriv_thm
⊢ ∀ x• ¬ Cos x = 0. ⇒ (Tan Deriv 1. + Tan x ^ 2) x
cotan_deriv_thm
⊢ ∀ x
fill• ¬ Sin x = 0. ⇒ (Cotan Deriv ~ (1. + Cotan x ^ 2)) x
sec_deriv_thm
⊢ ∀ x• ¬ Cos x = 0. ⇒ (Sec Deriv Sec x * Tan x) x
cosec_deriv_thm
⊢ ∀ x
fill• ¬ Sin x = 0.
fill⇒ (Cosec Deriv ~ (Cosec x) * Cotan x) x
cos_0_less_thm
⊢ ∀ x• ~ (1 / 2) * π < x ∧ x < 1 / 2 * π ⇒ 0. < Cos x
ArcSin_consistent
⊢ Consistent
fill(λ ArcSin'
fill• (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin' (Sin x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1.
fill⇒ Sin (ArcSin' x) = x ∧ ArcSin' Cts x))
arc_sin_def
⊢ (∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin (Sin x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1. ⇒ Sin (ArcSin x) = x ∧ ArcSin Cts x)
sin_arc_sin_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ Sin (ArcSin x) = x
arc_sin_sin_thm
⊢ ∀ x• Abs x ≤ 1 / 2 * π ⇒ ArcSin (Sin x) = x
arc_sin_cts_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ ArcSin Cts x
abs_arc_sin_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ Abs (ArcSin x) ≤ 1 / 2 * π
cos_arc_sin_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ Cos (ArcSin x) = Sqrt (1. - x ^ 2)
arc_sin_1_minus_1_thm
⊢ ArcSin 1. = 1 / 2 * π ∧ ArcSin (~ 1.) = ~ (1 / 2) * π
arc_sin_deriv_thm
⊢ ∀ x
fill• Abs x < 1.
fill⇒ (ArcSin Deriv Sqrt (1. - x ^ 2) -1) x
ArcCos_consistent
⊢ Consistent
fill(λ ArcCos'
fill• (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos' (Cos x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1.
fill⇒ Cos (ArcCos' x) = x ∧ ArcCos' Cts x))
arc_cos_def
⊢ (∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos (Cos x) = x)
fill∧ (∀ x
fill• Abs x ≤ 1. ⇒ Cos (ArcCos x) = x ∧ ArcCos Cts x)
cos_arc_cos_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ Cos (ArcCos x) = x
arc_cos_cos_thm
⊢ ∀ x• 0. ≤ x ∧ x ≤ π ⇒ ArcCos (Cos x) = x
arc_cos_cts_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ ArcCos Cts x
abs_arc_cos_thm
⊢ ∀ x• Abs x ≤ 1. ⇒ 0. ≤ ArcCos x ∧ ArcCos x ≤ π
sinh_deriv_thm
⊢ ∀ x• (Sinh Deriv Cosh x) x
cosh_deriv_thm
⊢ ∀ x• (Cosh Deriv Sinh x) x
cosh_0_less_thm
⊢ ∀ x• 0. < Cosh x
cosh_non_0_thm
⊢ ∀ x• ¬ Cosh x = 0.
sinh_non_0_thm
⊢ ∀ x• Sinh x = 0. ⇔ x = 0.
cosh_squared_minus_sinh_squared_thm
⊢ ∀ x• Cosh x ^ 2 - Sinh x ^ 2 = 1.
tanh_deriv_thm
⊢ ∀ x• (Tanh Deriv 1. - Tanh x ^ 2) x
cotanh_deriv_thm
⊢ ∀ x• ¬ x = 0. ⇒ (Cotanh Deriv 1. - Cotanh x ^ 2) x
sech_deriv_thm
⊢ ∀ x• (Sech Deriv ~ (Sech x) * Tanh x) x
cosech_deriv_thm
⊢ ∀ x
fill• ¬ x = 0. ⇒ (Cosech Deriv ~ (Cosech x) * Cotanh x) x
sinh_cts_thm
⊢ ∀ x• Sinh Cts x
cosh_cts_thm
⊢ ∀ x• Cosh Cts x
sinh_mono_thm
⊢ ∀ x y• x < y ⇒ Sinh x < Sinh y
sinh_cosh_0_thm
⊢ Sinh 0. = 0. ∧ Cosh 0. = 1.
sinh_cosh_minus_thm
⊢ ∀ x• Sinh (~ x) = ~ (Sinh x) ∧ Cosh (~ x) = Cosh x
ArcSinh_consistent
⊢ Consistent
fill(λ ArcSinh'
fill• ∀ x
fill• ArcSinh' (Sinh x) = x
fill∧ Sinh (ArcSinh' x) = x
fill∧ ArcSinh' Cts x)
arc_sinh_def
⊢ ∀ x
fill• ArcSinh (Sinh x) = x
fill∧ Sinh (ArcSinh x) = x
fill∧ ArcSinh Cts x
sqrt_1_plus_sinh_squared_thm
⊢ ∀ x• Sqrt (1. + Sinh x ^ 2) = Cosh x
cosh_arc_sinh_thm
⊢ ∀ x• Cosh (ArcSinh x) = Sqrt (1. + x ^ 2)
arc_sinh_deriv_thm
⊢ ∀ x• (ArcSinh Deriv Sqrt (1. + x ^ 2) -1) x
gauge_∩_thm
⊢ ∀ G1 G2
fill• G1 ∈ Gauge ∧ G2 ∈ Gauge
fill⇒ (λ x• G1 x ∩ G2 x) ∈ Gauge
gauge_o_minus_thm
⊢ ∀ G• G ∈ Gauge ⇒ (λ x• {t|~ t ∈ G (~ x)}) ∈ Gauge
gauge_o_plus_thm
⊢ ∀ G h
fill• G ∈ Gauge ⇒ (λ x• {t|t + h ∈ G (x + h)}) ∈ Gauge
gauge_o_times_thm
⊢ ∀ c G
fill• G ∈ Gauge ∧ ¬ c = 0.
fill⇒ (λ x• {t|c * t ∈ G (c * x)}) ∈ Gauge
gauge_refinement_thm
⊢ ∀ G1 G2
fill• G1 ∈ Gauge ∧ G2 ∈ Gauge
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ x• G x ⊆ G1 x)
fill∧ (∀ x• G x ⊆ G2 x))
gauge_refine_3_thm
⊢ ∀ G1 G2 G3
fill• G1 ∈ Gauge ∧ G2 ∈ Gauge ∧ G3 ∈ Gauge
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ x• G x ⊆ G1 x)
fill∧ (∀ x• G x ⊆ G2 x)
fill∧ (∀ x• G x ⊆ G3 x))
fine_refinement_thm
⊢ ∀ G1 G2 t I n
fill• (∀ x• G1 x ⊆ G2 x) ∧ (t, I, n) ∈ G1 Fine
fill⇒ (t, I, n) ∈ G2 Fine
chosen_tag_thm
⊢ ∀ a
fill• ∃ G1
fill• G1 ∈ Gauge
fill∧ (∀ G2
fill• G2 ∈ Gauge ∧ (∀ x• G2 x ⊆ G1 x)
fill⇒ (∀ t I n m
fill• m < n
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G2 Fine
fill∧ a
fill∈ ClosedInterval (I m) (I (m + 1))
fill⇒ t m = a))
chosen_tags_thm
⊢ ∀ list
fill• ∃ G1
fill• G1 ∈ Gauge
fill∧ (∀ G2
fill• G2 ∈ Gauge ∧ (∀ x• G2 x ⊆ G1 x)
fill⇒ (∀ t I n m a
fill• m < n
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G2 Fine
fill∧ a
fill∈ ClosedInterval (I m) (I (m + 1))
fill∧ a ∈ Elems list
fill⇒ t m = a))
riemann_gauge_thm
⊢ ∀ e
fill• 0. < e
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ t I n m
fill• m < n
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G Fine
fill⇒ I (m + 1) - I m < e))
tagged_partition_∃_thm
cousin_lemma
⊢ ∀ G a b
fill• G ∈ Gauge ∧ a ≤ b
fill⇒ (∃ t I n
fill• I 0 = a
fill∧ I n = b
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G Fine)
riemann_sum_induction_thm
⊢ ∀ f t I n
fill• RiemannSum f (t, I, 0) = 0.
fill∧ RiemannSum f (t, I, n + 1)
fill= RiemannSum f (t, I, n)
fill+ f (t n) * (I (n + 1) - I n)
series_induction_thm1
⊢ ∀ s n
fill• Series s (n + 1) = s 0 + Series (λ m• s (m + 1)) n
ℝ_abs_series_thm
⊢ ∀ s n• Abs (Series s n) ≤ Series (λ m• Abs (s m)) n
riemann_sum_induction_thm1
⊢ ∀ f t I n
fill• RiemannSum f (t, I, 0) = 0.
fill∧ RiemannSum f (t, I, n + 1)
fill= f (t 0) * (I 1 - I 0)
fill+ RiemannSum
fillf
fill((λ m• t (m + 1)), (λ m• I (m + 1)), n)
riemann_sum_plus_thm
⊢ ∀ f g t I n
fill• RiemannSum (λ x• f x + g x) (t, I, n)
fill= RiemannSum f (t, I, n) + RiemannSum g (t, I, n)
riemann_sum_const_times_thm
⊢ ∀ f c t I n
fill• RiemannSum (λ x• c * f x) (t, I, n)
fill= c * RiemannSum f (t, I, n)
riemann_sum_minus_thm
⊢ ∀ f t I n
fill• RiemannSum (λ x• ~ (f x)) (t, I, n)
fill= ~ (RiemannSum f (t, I, n))
riemann_sum_local_thm
⊢ ∀ f t I s J n
fill• (∀ m• m < n ⇒ t m = s m) ∧ (∀ m• m ≤ n ⇒ I m = J m)
fill⇒ RiemannSum f (t, I, n) = RiemannSum f (s, J, n)
riemann_sum_o_minus_thm
⊢ ∀ f t I n
fill• RiemannSum f (t, I, n)
fill= RiemannSum
fill(λ x• f (~ x))
fill((λ m• ~ (t (n - 1 - m))),
fill(λ m• ~ (I (n - m))), n)
riemann_sum_o_times_thm
⊢ ∀ f t I n c
fill• ¬ c = 0.
fill⇒ RiemannSum (λ x• f (c * x)) (t, I, n)
fill= c -1
fill* RiemannSum
fillf
fill((λ m• c * t m), (λ m• c * I m), n)
partition_reverse_clauses
⊢ ∀ f t I n G
fill• ((t, I, n) ∈ TaggedPartition
fill⇒ ((λ m• ~ (t (n - 1 - m))),
fill(λ m• ~ (I (n - m))), n)
fill∈ TaggedPartition)
fill∧ ((t, I, n) ∈ G Fine
fill⇒ ((λ m• ~ (t (n - 1 - m))),
fill(λ m• ~ (I (n - m))), n)
fill∈ (λ x• {t|~ t ∈ G (~ x)}) Fine)
tagged_partition_append_thm
⊢ ∀ s J m t I n
fill• (s, J, m) ∈ TaggedPartition
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ J m = I 0
fill⇒ ((λ k• if k < m then s k else t (k - m)),
fill(λ k• if k ≤ m then J k else I (k - m)),
fillm + n)
fill∈ TaggedPartition
fine_append_thm
⊢ ∀ G s J m t I n
fill• (s, J, m) ∈ G Fine ∧ (t, I, n) ∈ G Fine ∧ J m = I 0
fill⇒ ((λ k• if k < m then s k else t (k - m)),
fill(λ k• if k ≤ m then J k else I (k - m)),
fillm + n)
fill∈ G Fine
riemann_sum_0_thm
⊢ ∀ t I n• RiemannSum (λ x• 0.) (t, I, n) = 0.
riemann_sum_append_thm
⊢ ∀ f t I m n
fill• RiemannSum f (t, I, m + n)
fill= RiemannSum f (t, I, m)
fill+ RiemannSum
fillf
fill((λ k• t (m + k)), (λ k• I (m + k)), n)
riemann_sum_¬_0_thm
⊢ ∀ f t I n
fill• ¬ RiemannSum f (t, I, n) = 0.
fill⇒ (∃ m
fill• m < n
fill∧ ¬ f (t m) = 0.
fill∧ RiemannSum f (t, I, n)
fill= RiemannSum f (t, I, m + 1))
partition_mono_thm
⊢ ∀ t I n k m
fill• (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n
fill⇒ I k < I (m + 1)
tag_mono_thm
⊢ ∀ t I n k m
fill• (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n
fill⇒ t k ≤ t m
tag_upper_bound_thm
⊢ ∀ t I n k m
fill• (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n
fill⇒ t k ≤ I (m + 1)
tag_lower_bound_thm
⊢ ∀ t I n k m
fill• (t, I, n) ∈ TaggedPartition ∧ k ≤ m ∧ m < n
fill⇒ I k ≤ t m
subpartition_thm
⊢ ∀ n m t I
fill• m ≤ n ∧ (t, I, n) ∈ TaggedPartition
fill⇒ (t, I, m) ∈ TaggedPartition
subpartition_fine_thm
⊢ ∀ n m t I n G
fill• m ≤ n ∧ (t, I, n) ∈ G Fine ⇒ (t, I, m) ∈ G Fine
riemann_sum_local_thm1
⊢ ∀ f g t I n
fill• (∀ x• I 0 ≤ x ∧ x ≤ I n ⇒ f x = g x)
fill∧ (t, I, n) ∈ TaggedPartition
fill⇒ RiemannSum f (t, I, n) = RiemannSum g (t, I, n)
riemann_sum_0_≤_thm
⊢ ∀ f t I n
fill• (∀ x• 0. ≤ f x) ∧ (t, I, n) ∈ TaggedPartition
fill⇒ 0. ≤ RiemannSum f (t, I, n)
tag_unique_thm
⊢ ∀ t I n k m
fill• (t, I, n) ∈ TaggedPartition
fill∧ k < m
fill∧ m < n
fill∧ t k = t m
fill⇒ m = k + 1
partition_cover_thm
⊢ ∀ t I n x
fill• (t, I, n) ∈ TaggedPartition ∧ I 0 < x ∧ x ≤ I n
fill⇒ (∃ m• m < n ∧ I m < x ∧ x ≤ I (m + 1))
partition_cover_thm1
⊢ ∀ t I n x
fill• (t, I, n) ∈ TaggedPartition ∧ I 0 ≤ x ∧ x < I n
fill⇒ (∃ m• m < n ∧ I m ≤ x ∧ x < I (m + 1))
riemann_sum_χ_singleton_thm
⊢ ∀ c t I n
fill• (t, I, n) ∈ TaggedPartition
fill⇒ RiemannSum (χ {c}) (t, I, n) = 0.
fill∨ (∃ m
fill• m < n
fill∧ RiemannSum (χ {c}) (t, I, n)
fill= I (m + 1) - I m)
fill∨ (∃ m
fill• m + 1 < n
fill∧ RiemannSum (χ {c}) (t, I, n)
fill= I (m + 2) - I m)
int_ℝ_plus_thm
⊢ ∀ f g c d
fill• f IntR c ∧ g IntR d
fill⇒ (λ x• f x + g x) IntR c + d
int_ℝ_minus_thm
⊢ ∀ f c• f IntR c ⇒ (λ x• ~ (f x)) IntR ~ c
int_ℝ_0_thm
⊢ (λ x• 0.) IntR 0.
int_ℝ_const_times_thm
⊢ ∀ f c d• f IntR d ⇒ (λ x• c * f x) IntR c * d
int_ℝ_diff_0_thm
⊢ ∀ f g c
fill• (λ x• f x - g x) IntR 0. ⇒ (f IntR c ⇔ g IntR c)
int_ℝ_unique_thm
⊢ ∀ f c d• f IntR c ∧ f IntR d ⇒ c = d
int_ℝ_0_≤_thm
⊢ ∀ f c• (∀ x• 0. ≤ f x) ∧ f IntR c ⇒ 0. ≤ c
int_ℝ_≤_thm
⊢ ∀ f g c d
fill• (∀ x• f x ≤ g x) ∧ f IntR c ∧ g IntR d ⇒ c ≤ d
int_ℝ_0_dominated_thm
⊢ ∀ f g
fill• (∀ x• 0. ≤ f x) ∧ (∀ x• f x ≤ g x) ∧ g IntR 0.
fill⇒ f IntR 0.
int_ℝ_χ_singleton_lemma
⊢ ∀ G e c t I n
fill• 0. < e
fill∧ G ∈ Gauge
fill∧ (∀ t I n m
fill• m < n
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G Fine
fill⇒ I (m + 1) - I m < e)
fill∧ (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum (χ {c}) (t, I, n)) < 2. * e
int_ℝ_χ_singleton_thm
⊢ ∀ c• χ {c} IntR 0.
int_ℝ_singleton_support_thm
⊢ ∀ f c• (∀ x• ¬ f x = 0. ⇒ x = c) ⇒ f IntR 0.
int_ℝ_finite_support_thm
⊢ ∀ f list
fill• (∀ x• ¬ f x = 0. ⇒ x ∈ Elems list) ⇒ f IntR 0.
int_ℝ_χ_0_⊆_thm
⊢ ∀ A B• A ⊆ B ∧ χ B IntR 0. ⇒ χ A IntR 0.
int_ℝ_χ_0_∩_thm
⊢ ∀ A B• χ A IntR 0. ⇒ χ (A ∩ B) IntR 0.
χ_∪_∩_thm
⊢ ∀ A B x• χ (A ∪ B) x = χ A x + χ B x - χ (A ∩ B) x
int_ℝ_χ_0_∪_thm
⊢ ∀ A B
fill• χ A IntR 0. ∧ χ B IntR 0. ⇒ χ (A ∪ B) IntR 0.
int_half_infinite_interval_thm
⊢ ∀ f c a• (f Int c) {x|a ≤ x} ⇔ (f Int c) {x|a < x}
chosen_value_thm
⊢ ∀ y f c A
fill• (f Int c) A
fill⇔ ((λ x• if x = y then 0. else f x) Int c) A
int_interval_thm
⊢ ∀ f g a b c
fill• (f Int c) (ClosedInterval a b)
fill⇔ (f Int c) (OpenInterval a b)
int_ℝ_o_minus_thm
⊢ ∀ f c• f IntR c ⇔ (λ x• f (~ x)) IntR c
int_ℝ_o_plus_thm
⊢ ∀ f c h• f IntR c ⇔ (λ x• f (x + h)) IntR c
int_ℝ_o_times_thm
⊢ ∀ f c d
fill• ¬ 0. = d ∧ f IntR c
fill⇒ (λ x• f (d * x)) IntR Abs d -1 * c
int_ℝ_support_bounded_below_thm
⊢ ∀ a c f
fill• (∀ x• x ≤ a ⇒ f x = 0.)
fill⇒ (f IntR c
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G b
fill• G ∈ Gauge
fill∧ a < b
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ b < I n
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e))))
int_support_bounded_below_lemma
⊢ ∀ a f g c
fill• (∀ x• a < x ⇒ f x = g x)
fill⇒ ((∀ e
fill• 0. < e
fill⇒ (∃ G b
fill• G ∈ Gauge
fill∧ a < b
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ b < I n
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e)))
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G b
fill• G ∈ Gauge
fill∧ a < b
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ b < I n
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum g (t, I, n) - c)
fill< e))))
int_bounded_below_thm
⊢ ∀ a b c f
fill• (f Int c) {x|a ≤ x}
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G b
fill• G ∈ Gauge
fill∧ a < b
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ b < I n
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e)))
int_ℝ_bounded_support_thm
⊢ ∀ a b c f
fill• a < b
fill∧ (∀ x• x ≤ a ⇒ f x = 0.)
fill∧ (∀ x• b ≤ x ⇒ f x = 0.)
fill⇒ (f IntR c
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ I n = b
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e))))
bounded_int_thm
⊢ ∀ a b c f
fill• a < b
fill⇒ ((f Int c) (ClosedInterval a b)
fill⇔ (∀ e
fill• 0. < e
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ t I n
fill• (t, I, n) ∈ TaggedPartition
fill∧ I 0 = a
fill∧ I n = b
fill∧ (t, I, n) ∈ G Fine
fill⇒ Abs (RiemannSum f (t, I, n) - c)
fill< e))))
bounded_int_local_thm
⊢ ∀ a b f g c
fill• a < b ∧ (∀ x• x ∈ ClosedInterval a b ⇒ f x = g x)
fill⇒ ((g Int c) (ClosedInterval a b)
fill⇔ (f Int c) (ClosedInterval a b))
straddle_thm
⊢ ∀ f df x e
fill• (f Deriv df x) x ∧ 0. < e
fill⇒ (∃ d
fill• 0. < d
fill∧ (∀ u v
fill• u ∈ OpenInterval (x - d) (x + d)
fill∧ v ∈ OpenInterval (x - d) (x + d)
fill∧ u ≤ x
fill∧ x ≤ v
fill⇒ Abs (df x * (v - u) - (f v - f u))
fill≤ e * (v - u)))
straddle_gauge_thm
⊢ ∀ A e f df
fill• (∀ x• x ∈ A ⇒ (f Deriv df x) x) ∧ 0. < e
fill⇒ (∃ G
fill• G ∈ Gauge
fill∧ (∀ t I n m
fill• (t, I, n) ∈ TaggedPartition
fill∧ (t, I, n) ∈ G Fine
fill∧ m < n
fill∧ t m ∈ A
fill⇒ Abs
fill(df (t m) * (I (m + 1) - I m)
fill- (f (I (m + 1)) - f (I m)))
fill≤ e * (I (m + 1) - I m)))
int_deriv_thm2
⊢ ∀ a b sf f
fill• a < b
fill∧ (∀ x• a ≤ x ∧ x < b ⇒ (sf Deriv f x) x)
fill∧ sf Cts b
fill⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm3
⊢ ∀ a b sf f
fill• a < b
fill∧ (∀ x• a < x ∧ x ≤ b ⇒ (sf Deriv f x) x)
fill∧ sf Cts a
fill⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm
⊢ ∀ a b sf f
fill• a < b
fill∧ (∀ x• a < x ∧ x < b ⇒ (sf Deriv f x) x)
fill∧ sf Cts a
fill∧ sf Cts b
fill⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_deriv_thm1
⊢ ∀ a b sf f
fill• a < b
fill∧ (∀ x
fill• x ∈ ClosedInterval a b ⇒ (sf Deriv f x) x)
fill⇒ (f Int sf b - sf a) (ClosedInterval a b)
int_ℝ_χ_interval_thm
⊢ ∀ a b• a ≤ b ⇒ χ (ClosedInterval a b) IntR b - a
int_example_thm
⊢ ((λ x• Sqrt (1. - x ^ 2) -1) Int π)
fill(ClosedInterval (~ 1.) 1.)
int_recip_thm
⊢ ∀ a b
fill• 0. < a ∧ a < b
fill⇒ ((λ x• x -1) Int Log b - Log a)
fill(ClosedInterval a b)
log_minus_log_estimate_thm
⊢ ∀ a b
fill• 0. < a ∧ a < b ⇒ Log b - Log a ≤ (b - a) * a -1
harmonic_series_estimate_thm
⊢ ∀ m
fill• Log (ℕℝ (m + 1)) ≤ Series (λ m• ℕℝ (m + 1) -1) m
harmonic_series_divergent_thm
⊢ ∀ c• ¬ Series (λ m• ℕℝ (m + 1) -1) -> c
area_unique_thm
⊢ ∀ A c d• A Area c ∧ A Area d ⇒ c = d
area_translate_thm
⊢ ∀ A c u v
fill• A Area c ⇒ {(x, y)|(x + u, y + v) ∈ A} Area c
area_dilate_thm
⊢ ∀ A c d e
fill• A Area c ∧ ¬ d = 0. ∧ ¬ e = 0.
fill⇒ {(x, y)|(d -1 * x, e -1 * y) ∈ A}
fillArea Abs d * Abs e * c
area_dilate_thm1
⊢ ∀ A c d
fill• A Area c ∧ ¬ d = 0.
fill⇒ {(x, y)|(d -1 * x, d -1 * y) ∈ A}
fillArea d ^ 2 * c
area_empty_thm
⊢ {} Area 0.
area_∪_thm
⊢ ∀ A B c d y
fill• A Area c ∧ B Area d ∧ A ∩ B Area y
fill⇒ A ∪ B Area c + d - y
area_∩_thm
⊢ ∀ A B c d y
fill• A Area c ∧ B Area d ∧ A ∪ B Area y
fill⇒ A ∩ B Area c + d - y
area_rectangle_thm
⊢ ∀ w h
fill• 0. ≤ h ∧ 0. ≤ w
fill⇒ {(x, y)
fill|x ∈ ClosedInterval 0. w
fill∧ y ∈ ClosedInterval 0. h}
fillArea w * h
area_circle_lemma1
⊢ ∀ x
fill• Abs x < 1.
fill⇒ ((λ x• x * Sqrt (1. - x ^ 2) + ArcSin x)
fillDeriv 2. * Sqrt (1. - x ^ 2))
fillx
area_circle_lemma2
⊢ ∀ x• Abs x ≤ 1. ⇒ 0. ≤ 1. - x ^ 2
area_circle_lemma3
⊢ ∀ x
fill• Abs x ≤ 1.
fill⇒ (λ x• x * Sqrt (1. - x ^ 2) + ArcSin x) Cts x
area_circle_lemma4
⊢ ∀ r x y
fill• Abs x ≤ r
fill⇒ (Sqrt (x ^ 2 + y ^ 2) ≤ r
fill⇔ Abs y ≤ Sqrt (r ^ 2 - x ^ 2))
area_circle_int_thm
⊢ ((λ x• 2. * Sqrt (1. - x ^ 2)) Int π)
fill(ClosedInterval (~ 1.) 1.)
area_unit_circle_thm
⊢ {(x, y)|Sqrt (x ^ 2 + y ^ 2) ≤ 1.} Area π
circle_dilate_thm
⊢ ∀ r
fill• 0. < r
fill⇒ {(x, y)|Sqrt (x ^ 2 + y ^ 2) ≤ r}
fill= {(x, y)
fill|Sqrt ((r -1 * x) ^ 2 + (r -1 * y) ^ 2)
fill≤ 1.}
area_circle_thm
⊢ ∀ r
fill• 0. < r
fill⇒ {(x, y)|Sqrt (x ^ 2 + y ^ 2) ≤ r}
fillArea π * r ^ 2
buffon_needle_lemma
⊢ let S
fill= {(θ, d)
fill|θ ∈ ClosedInterval 0. π
fill∧ d ∈ ClosedInterval 0. 1.}
fillin let x_axis = {(x, y)|y = 0.}
fillin let needle (θ, d)
fill= {(x, y)
fill|∃ t
fill• t ∈ ClosedInterval 0. 1.
fill∧ x = t * Cos θ
fill∧ y = d - t * Sin θ}
fillin let X
fill= {(θ, d)
fill|(θ, d) ∈ S
fill∧ ¬ needle (θ, d) ∩ x_axis = {}}
fillin X Area 2.
buffon_needle_thm
⊢ let S
fill= {(θ, d)
fill|θ ∈ ClosedInterval 0. π
fill∧ d ∈ ClosedInterval 0. 1.}
fillin let x_axis = {(x, y)|y = 0.}
fillin let needle (θ, d)
fill= {(x, y)
fill|∃ t
fill• t ∈ ClosedInterval 0. 1.
fill∧ x = t * Cos θ
fill∧ y = d - t * Sin θ}
fillin let X
fill= {(θ, d)
fill|(θ, d) ∈ S
fill∧ ¬ needle (θ, d) ∩ x_axis = {}}
fillin X ⊆ S
fill∧ (∃ x s
fill• ¬ s = 0.
fill∧ X Area x
fill∧ S Area s
fill∧ x / s = 2. / π)

up quick index

privacy policy

Created:

V