Skip to content

Commit

Permalink
Added lots of nice new material from Andrea Gabrielli and Marco Maggesi,
Browse files Browse the repository at this point in the history 
with useful theorems in several areas:

        * More properties of sup and inf including relational versions

        * Theory of limits superior and inferior (limup and liminf)

        * A few miscellaneous lemmas about convergence and series

        * The root test for series convergence (scalar and vector)

        * Cauchy-Hadamard results on power series radius of convergence

List of new theorems:

        CAUCHY_HADAMARD_RADIUS
        CAUCHY_HADAMARD_RADIUS_ABSCONV
        CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE
        CAUCHY_HADAMARD_RADIUS_DERIVATIVE
        CAUCHY_HADAMARD_RADIUS_UNIFORM
        CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE
        COMPACT_SHRINK_ENCLOSING_BALL
        COMPACT_SHRINK_ENCLOSING_BALL_INFTY
        EVENTUALLY_EQ_MP
        EVENTUALLY_IFF
        EVENTUALLY_LBOUND_LE_SEQUENTIALLY
        EVENTUALLY_SEQUENTIALLY_WITHIN
        EVENTUALLY_UBOUND_LE_SEQUENTIALLY
        HAS_INF
        HAS_INF_APPROACH
        HAS_INF_INF
        HAS_INF_LBOUND
        HAS_INF_LE
        HAS_LIMINF
        HAS_LIMINF_AT
        HAS_LIMINF_AT_REALLIM_INF
        HAS_LIMINF_EVENTUALLY_LBOUND
        HAS_LIMINF_IMP_LBOUND_LE
        HAS_LIMINF_LBOUND
        HAS_LIMINF_LE
        HAS_LIMINF_NOT_LBOUND
        HAS_LIMINF_SEQUENTIALLY
        HAS_LIMINF_SEQUENTIALLY_IMP_REALLIM_INF
        HAS_LIMINF_SEQUENTIALLY_REALLIM_INF
        HAS_LIMINF_SEQUENTIALLY_WITHIN
        HAS_LIMINF_TRANSFORM
        HAS_LIMSUP
        HAS_LIMSUP_AT
        HAS_LIMSUP_AT_REALLIM_SUP
        HAS_LIMSUP_EVENTUALLY_UBOUND
        HAS_LIMSUP_IMP_UBOUND_LE
        HAS_LIMSUP_LE
        HAS_LIMSUP_MUL_REALLIM_LEFT
        HAS_LIMSUP_MUL_REALLIM_RIGHT
        HAS_LIMSUP_NOT_UBOUND
        HAS_LIMSUP_SEQUENTIALLY
        HAS_LIMSUP_SEQUENTIALLY_IMP_REALLIM_SUP
        HAS_LIMSUP_SEQUENTIALLY_REALLIM_SUP
        HAS_LIMSUP_SEQUENTIALLY_WITHIN
        HAS_LIMSUP_SEQUENTIALLY_WITHIN_LBOUND_ZERO
        HAS_LIMSUP_TRANSFORM
        HAS_LIMSUP_UBOUND
        HAS_SUP
        HAS_SUP_APPROACH
        HAS_SUP_LE
        HAS_SUP_SUP
        HAS_SUP_UBOUND
        INF_APPROACH
        INF_EXISTS
        LIMINF_EXISTS
        LIMSUP_EXISTS
        REALLIM_EVENTUALLY_LBOUND
        REALLIM_EVENTUALLY_UBOUND
        REALLIM_IMP_HAS_LIMINF
        REALLIM_IMP_HAS_LIMSUP
        REALLIM_ROOT_REFL
        REALLIM_SEQUENTIALLY_WITHIN
        REAL_CAUCHY_HADAMARD_RADIUS
        REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV
        REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE
        REAL_CAUCHY_HADAMARD_RADIUS_DERIVATIVE
        REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM
        REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE
        REAL_SERIES_ROOT_TEST
        REAL_SUMMABLE_FINITE
        REAL_SUMMABLE_POS_SUBSET
        SERIES_NORMCONV_IMP_CONV
        SERIES_ROOT_TEST
        SUMMABLE_FINITE
        SUP_APPROACH
        SUP_EXISTS
        TRIVIAL_LIMIT_SEQUENTIALLY_WITHIN
        has_inf
        has_liminf
        has_limsup
        has_sup

Also type-generalized one existing theorem PASTECART_INJ, which had a
pointless restriction to ":real^N" where in fact any ":A^N" works.
  • Loading branch information
@jrh13
jrh13 committed Apr 10, 2017
1 parent 75f772e commit 2430ee0
Show file tree
Hide file tree
Showing 9 changed files with 1,936 additions and 71 deletions.
82 changes: 82 additions & 0 deletions CHANGES
View file
Expand Up @@ -8,6 +8,88 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Sat 8th Apr 2017 cart.ml

Type-generalized PASTECART_INJ which had a pointless restriction to ":real".

Sat 8th Apr 2017 sets.ml

Added a number of new theorems from Andrea Gabrielli and Marco Maggesi, giving
some additional properties of sup and inf and using useful relational versions
"has_sup" and "has_inf" to express some properties more nicely:

has_inf =
|- !s b. s has_inf b <=> (!c. (!x. x IN s ==> c <= x) <=> c <= b)

has_sup =
|- !s b. s has_sup b <=> (!c. (!x. x IN s ==> x <= c) <=> b <= c)

HAS_INF =
|- !s l.
s has_inf l <=>
~(s = {}) /\
(!x. x IN s ==> l <= x) /\
(!c. l < c ==> (?x. x IN s /\ x < c))

HAS_INF_APPROACH =
|- !s l c. s has_inf l /\ l < c ==> (?x. x IN s /\ x < c)

HAS_INF_INF =
|- !s l.
s has_inf l <=>
~(s = {}) /\ (?b. !x. x IN s ==> b <= x) /\ inf s = l

HAS_INF_LBOUND =
|- !s b x. s has_inf b /\ x IN s ==> b <= x

HAS_INF_LE =
|- !s t l m.
s has_inf l /\
t has_inf m /\
(!y. y IN t ==> (?x. x IN s /\ x <= y))
==> l <= m

HAS_SUP =
|- !s l.
s has_sup l <=>
~(s = {}) /\
(!x. x IN s ==> x <= l) /\
(!c. c < l ==> (?x. x IN s /\ c < x))

HAS_SUP_APPROACH =
|- !s l c. s has_sup l /\ c < l ==> (?x. x IN s /\ c < x)

HAS_SUP_LE =
|- !s t l m.
s has_sup l /\
t has_sup m /\
(!y. y IN t ==> (?x. x IN s /\ y <= x))
==> m <= l

HAS_SUP_SUP =
|- !s l.
s has_sup l <=>
~(s = {}) /\ (?b. !x. x IN s ==> x <= b) /\ sup s = l

HAS_SUP_UBOUND =
|- !s b x. s has_sup b /\ x IN s ==> x <= b

INF_APPROACH =
|- !s c.
~(s = {}) /\ (?b. !x. x IN s ==> b <= x) /\ inf s < c
==> (?x. x IN s /\ x < c)

INF_EXISTS =
|- !s. (?l. s has_inf l) <=> ~(s = {}) /\ (?b. !x. x IN s ==> b <= x)

SUP_APPROACH =
|- !s c.
~(s = {}) /\ (?b. !x. x IN s ==> x <= b) /\ c < sup s
==> (?x. x IN s /\ c < x)

SUP_EXISTS =
|- !s. (?l. s has_sup l) <=> ~(s = {}) /\ (?b. !x. x IN s ==> x <= b)

Wed 29th Mar 2017 arith.ml

Added some natural theorems that were missing:
Expand Down
81 changes: 81 additions & 0 deletions Multivariate/complex_database.ml
View file
Expand Up @@ -1573,6 +1573,12 @@ theorems :=
"CAUCHY_CONVERGENT_SUBSEQUENCE",CAUCHY_CONVERGENT_SUBSEQUENCE;
"CAUCHY_DERIVATIVE_INTEGRAL_CIRCLEPATH",CAUCHY_DERIVATIVE_INTEGRAL_CIRCLEPATH;
"CAUCHY_EQ_SUMMABLE",CAUCHY_EQ_SUMMABLE;
"CAUCHY_HADAMARD_RADIUS",CAUCHY_HADAMARD_RADIUS;
"CAUCHY_HADAMARD_RADIUS_ABSCONV",CAUCHY_HADAMARD_RADIUS_ABSCONV;
"CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE",CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE;
"CAUCHY_HADAMARD_RADIUS_DERIVATIVE",CAUCHY_HADAMARD_RADIUS_DERIVATIVE;
"CAUCHY_HADAMARD_RADIUS_UNIFORM",CAUCHY_HADAMARD_RADIUS_UNIFORM;
"CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE",CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE;
"CAUCHY_HAS_PATH_INTEGRAL_HIGHER_DERIVATIVE_CIRCLEPATH",CAUCHY_HAS_PATH_INTEGRAL_HIGHER_DERIVATIVE_CIRCLEPATH;
"CAUCHY_HIGHER_COMPLEX_DERIVATIVE_BOUND",CAUCHY_HIGHER_COMPLEX_DERIVATIVE_BOUND;
"CAUCHY_HIGHER_DERIVATIVE_INTEGRAL_CIRCLEPATH",CAUCHY_HIGHER_DERIVATIVE_INTEGRAL_CIRCLEPATH;
Expand Down Expand Up @@ -2287,6 +2293,8 @@ theorems :=
"COMPACT_SEGMENT",COMPACT_SEGMENT;
"COMPACT_SEQUENCE_WITH_LIMIT",COMPACT_SEQUENCE_WITH_LIMIT;
"COMPACT_SEQUENCE_WITH_LIMIT_GEN",COMPACT_SEQUENCE_WITH_LIMIT_GEN;
"COMPACT_SHRINK_ENCLOSING_BALL",COMPACT_SHRINK_ENCLOSING_BALL;
"COMPACT_SHRINK_ENCLOSING_BALL_INFTY",COMPACT_SHRINK_ENCLOSING_BALL_INFTY;
"COMPACT_SIMPLEX",COMPACT_SIMPLEX;
"COMPACT_SIMPLE_PATH_IMAGE",COMPACT_SIMPLE_PATH_IMAGE;
"COMPACT_SING",COMPACT_SING;
Expand Down Expand Up @@ -4867,22 +4875,27 @@ theorems :=
"EVENTUALLY_AT_TOPOLOGICAL",EVENTUALLY_AT_TOPOLOGICAL;
"EVENTUALLY_AT_WITHIN",EVENTUALLY_AT_WITHIN;
"EVENTUALLY_AT_ZERO",EVENTUALLY_AT_ZERO;
"EVENTUALLY_EQ_MP",EVENTUALLY_EQ_MP;
"EVENTUALLY_FALSE",EVENTUALLY_FALSE;
"EVENTUALLY_FORALL",EVENTUALLY_FORALL;
"EVENTUALLY_HAPPENS",EVENTUALLY_HAPPENS;
"EVENTUALLY_HAPPENS_AT",EVENTUALLY_HAPPENS_AT;
"EVENTUALLY_IFF",EVENTUALLY_IFF;
"EVENTUALLY_IMP_WITHIN",EVENTUALLY_IMP_WITHIN;
"EVENTUALLY_IN_OPEN",EVENTUALLY_IN_OPEN;
"EVENTUALLY_IN_SEQUENTIALLY",EVENTUALLY_IN_SEQUENTIALLY;
"EVENTUALLY_LBOUND_LE_SEQUENTIALLY",EVENTUALLY_LBOUND_LE_SEQUENTIALLY;
"EVENTUALLY_MONO",EVENTUALLY_MONO;
"EVENTUALLY_MP",EVENTUALLY_MP;
"EVENTUALLY_NO_SUBSEQUENCE",EVENTUALLY_NO_SUBSEQUENCE;
"EVENTUALLY_SCALABLE_PROPERTY",EVENTUALLY_SCALABLE_PROPERTY;
"EVENTUALLY_SCALABLE_PROPERTY_EQ",EVENTUALLY_SCALABLE_PROPERTY_EQ;
"EVENTUALLY_SEQUENTIALLY",EVENTUALLY_SEQUENTIALLY;
"EVENTUALLY_SEQUENTIALLY_WITHIN",EVENTUALLY_SEQUENTIALLY_WITHIN;
"EVENTUALLY_SUBSEQUENCE",EVENTUALLY_SUBSEQUENCE;
"EVENTUALLY_TRIVIAL",EVENTUALLY_TRIVIAL;
"EVENTUALLY_TRUE",EVENTUALLY_TRUE;
"EVENTUALLY_UBOUND_LE_SEQUENTIALLY",EVENTUALLY_UBOUND_LE_SEQUENTIALLY;
"EVENTUALLY_WITHIN",EVENTUALLY_WITHIN;
"EVENTUALLY_WITHINREAL",EVENTUALLY_WITHINREAL;
"EVENTUALLY_WITHINREAL_LE",EVENTUALLY_WITHINREAL_LE;
Expand Down Expand Up @@ -6053,6 +6066,11 @@ theorems :=
"HAS_DOUBLE_INTEGRAL_CONVOLUTION",HAS_DOUBLE_INTEGRAL_CONVOLUTION;
"HAS_DOUBLE_INTEGRAL_PCROSS",HAS_DOUBLE_INTEGRAL_PCROSS;
"HAS_FRECHET_DERIVATIVE_UNIQUE_AT",HAS_FRECHET_DERIVATIVE_UNIQUE_AT;
"HAS_INF",HAS_INF;
"HAS_INF_APPROACH",HAS_INF_APPROACH;
"HAS_INF_INF",HAS_INF_INF;
"HAS_INF_LBOUND",HAS_INF_LBOUND;
"HAS_INF_LE",HAS_INF_LE;
"HAS_INTEGRAL",HAS_INTEGRAL;
"HAS_INTEGRAL_0",HAS_INTEGRAL_0;
"HAS_INTEGRAL_0_EQ",HAS_INTEGRAL_0_EQ;
Expand Down Expand Up @@ -6153,6 +6171,35 @@ theorems :=
"HAS_INTEGRAL_UNIONS_IMAGE",HAS_INTEGRAL_UNIONS_IMAGE;
"HAS_INTEGRAL_UNIQUE",HAS_INTEGRAL_UNIQUE;
"HAS_INTEGRAL_VSUM",HAS_INTEGRAL_VSUM;
"HAS_LIMINF",HAS_LIMINF;
"HAS_LIMINF_AT",HAS_LIMINF_AT;
"HAS_LIMINF_AT_REALLIM_INF",HAS_LIMINF_AT_REALLIM_INF;
"HAS_LIMINF_EVENTUALLY_LBOUND",HAS_LIMINF_EVENTUALLY_LBOUND;
"HAS_LIMINF_IMP_LBOUND_LE",HAS_LIMINF_IMP_LBOUND_LE;
"HAS_LIMINF_LBOUND",HAS_LIMINF_LBOUND;
"HAS_LIMINF_LE",HAS_LIMINF_LE;
"HAS_LIMINF_NOT_LBOUND",HAS_LIMINF_NOT_LBOUND;
"HAS_LIMINF_SEQUENTIALLY",HAS_LIMINF_SEQUENTIALLY;
"HAS_LIMINF_SEQUENTIALLY_IMP_REALLIM_INF",HAS_LIMINF_SEQUENTIALLY_IMP_REALLIM_INF;
"HAS_LIMINF_SEQUENTIALLY_REALLIM_INF",HAS_LIMINF_SEQUENTIALLY_REALLIM_INF;
"HAS_LIMINF_SEQUENTIALLY_WITHIN",HAS_LIMINF_SEQUENTIALLY_WITHIN;
"HAS_LIMINF_TRANSFORM",HAS_LIMINF_TRANSFORM;
"HAS_LIMSUP",HAS_LIMSUP;
"HAS_LIMSUP_AT",HAS_LIMSUP_AT;
"HAS_LIMSUP_AT_REALLIM_SUP",HAS_LIMSUP_AT_REALLIM_SUP;
"HAS_LIMSUP_EVENTUALLY_UBOUND",HAS_LIMSUP_EVENTUALLY_UBOUND;
"HAS_LIMSUP_IMP_UBOUND_LE",HAS_LIMSUP_IMP_UBOUND_LE;
"HAS_LIMSUP_LE",HAS_LIMSUP_LE;
"HAS_LIMSUP_MUL_REALLIM_LEFT",HAS_LIMSUP_MUL_REALLIM_LEFT;
"HAS_LIMSUP_MUL_REALLIM_RIGHT",HAS_LIMSUP_MUL_REALLIM_RIGHT;
"HAS_LIMSUP_NOT_UBOUND",HAS_LIMSUP_NOT_UBOUND;
"HAS_LIMSUP_SEQUENTIALLY",HAS_LIMSUP_SEQUENTIALLY;
"HAS_LIMSUP_SEQUENTIALLY_IMP_REALLIM_SUP",HAS_LIMSUP_SEQUENTIALLY_IMP_REALLIM_SUP;
"HAS_LIMSUP_SEQUENTIALLY_REALLIM_SUP",HAS_LIMSUP_SEQUENTIALLY_REALLIM_SUP;
"HAS_LIMSUP_SEQUENTIALLY_WITHIN",HAS_LIMSUP_SEQUENTIALLY_WITHIN;
"HAS_LIMSUP_SEQUENTIALLY_WITHIN_LBOUND_ZERO",HAS_LIMSUP_SEQUENTIALLY_WITHIN_LBOUND_ZERO;
"HAS_LIMSUP_TRANSFORM",HAS_LIMSUP_TRANSFORM;
"HAS_LIMSUP_UBOUND",HAS_LIMSUP_UBOUND;
"HAS_MEASURE",HAS_MEASURE;
"HAS_MEASURE_0",HAS_MEASURE_0;
"HAS_MEASURE_AFFINITY",HAS_MEASURE_AFFINITY;
Expand Down Expand Up @@ -6455,6 +6502,11 @@ theorems :=
"HAS_SIZE_SUC",HAS_SIZE_SUC;
"HAS_SIZE_UNION",HAS_SIZE_UNION;
"HAS_SIZE_UNIONS",HAS_SIZE_UNIONS;
"HAS_SUP",HAS_SUP;
"HAS_SUP_APPROACH",HAS_SUP_APPROACH;
"HAS_SUP_LE",HAS_SUP_LE;
"HAS_SUP_SUP",HAS_SUP_SUP;
"HAS_SUP_UBOUND",HAS_SUP_UBOUND;
"HAS_VECTOR_DERIVATIVE_ADD",HAS_VECTOR_DERIVATIVE_ADD;
"HAS_VECTOR_DERIVATIVE_AT_1D",HAS_VECTOR_DERIVATIVE_AT_1D;
"HAS_VECTOR_DERIVATIVE_AT_WITHIN",HAS_VECTOR_DERIVATIVE_AT_WITHIN;
Expand Down Expand Up @@ -7253,8 +7305,10 @@ theorems :=
"INFSUM_RESTRICT",INFSUM_RESTRICT;
"INFSUM_SUB",INFSUM_SUB;
"INFSUM_UNIQUE",INFSUM_UNIQUE;
"INF_APPROACH",INF_APPROACH;
"INF_CLOSURE",INF_CLOSURE;
"INF_EQ",INF_EQ;
"INF_EXISTS",INF_EXISTS;
"INF_FINITE",INF_FINITE;
"INF_FINITE_LEMMA",INF_FINITE_LEMMA;
"INF_INSERT",INF_INSERT;
Expand Down Expand Up @@ -8556,6 +8610,7 @@ theorems :=
"LIFT_SUM",LIFT_SUM;
"LIFT_TO_QUOTIENT_SPACE",LIFT_TO_QUOTIENT_SPACE;
"LIFT_TO_QUOTIENT_SPACE_UNIQUE",LIFT_TO_QUOTIENT_SPACE_UNIQUE;
"LIMINF_EXISTS",LIMINF_EXISTS;
"LIMIT_ATPOINTOF",LIMIT_ATPOINTOF;
"LIMIT_ATPOINTOF_METRIC",LIMIT_ATPOINTOF_METRIC;
"LIMIT_COMPONENTWISE",LIMIT_COMPONENTWISE;
Expand Down Expand Up @@ -8630,6 +8685,7 @@ theorems :=
"LIMPT_SING",LIMPT_SING;
"LIMPT_SUBSET",LIMPT_SUBSET;
"LIMPT_TRANSLATION_EQ",LIMPT_TRANSLATION_EQ;
"LIMSUP_EXISTS",LIMSUP_EXISTS;
"LIM_1_OVER_LOG",LIM_1_OVER_LOG;
"LIM_1_OVER_N",LIM_1_OVER_N;
"LIM_1_OVER_POWER",LIM_1_OVER_POWER;
Expand Down Expand Up @@ -11660,7 +11716,11 @@ theorems :=
"REALLIM_CONTINUOUS_FUNCTION",REALLIM_CONTINUOUS_FUNCTION;
"REALLIM_DIV",REALLIM_DIV;
"REALLIM_EVENTUALLY",REALLIM_EVENTUALLY;
"REALLIM_EVENTUALLY_LBOUND",REALLIM_EVENTUALLY_LBOUND;
"REALLIM_EVENTUALLY_UBOUND",REALLIM_EVENTUALLY_UBOUND;
"REALLIM_IM",REALLIM_IM;
"REALLIM_IMP_HAS_LIMINF",REALLIM_IMP_HAS_LIMINF;
"REALLIM_IMP_HAS_LIMSUP",REALLIM_IMP_HAS_LIMSUP;
"REALLIM_INV",REALLIM_INV;
"REALLIM_LBOUND",REALLIM_LBOUND;
"REALLIM_LE",REALLIM_LE;
Expand Down Expand Up @@ -11692,9 +11752,11 @@ theorems :=
"REALLIM_REAL_CONTINUOUS_FUNCTION",REALLIM_REAL_CONTINUOUS_FUNCTION;
"REALLIM_RMUL",REALLIM_RMUL;
"REALLIM_RMUL_EQ",REALLIM_RMUL_EQ;
"REALLIM_ROOT_REFL",REALLIM_ROOT_REFL;
"REALLIM_RPOW",REALLIM_RPOW;
"REALLIM_RPOW_COMPOSE",REALLIM_RPOW_COMPOSE;
"REALLIM_SEQUENTIALLY",REALLIM_SEQUENTIALLY;
"REALLIM_SEQUENTIALLY_WITHIN",REALLIM_SEQUENTIALLY_WITHIN;
"REALLIM_SUB",REALLIM_SUB;
"REALLIM_SUM",REALLIM_SUM;
"REALLIM_TRANSFORM",REALLIM_TRANSFORM;
Expand Down Expand Up @@ -11820,6 +11882,12 @@ theorems :=
"REAL_BOUNDS_LE",REAL_BOUNDS_LE;
"REAL_BOUNDS_LT",REAL_BOUNDS_LT;
"REAL_CARD_INTSEG_INT",REAL_CARD_INTSEG_INT;
"REAL_CAUCHY_HADAMARD_RADIUS",REAL_CAUCHY_HADAMARD_RADIUS;
"REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV",REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV;
"REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE",REAL_CAUCHY_HADAMARD_RADIUS_ABSCONV_DERIVATIVE;
"REAL_CAUCHY_HADAMARD_RADIUS_DERIVATIVE",REAL_CAUCHY_HADAMARD_RADIUS_DERIVATIVE;
"REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM",REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM;
"REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE",REAL_CAUCHY_HADAMARD_RADIUS_UNIFORM_DERIVATIVE;
"REAL_CLOSED",REAL_CLOSED;
"REAL_CLOSED_DIFF",REAL_CLOSED_DIFF;
"REAL_CLOSED_EMPTY",REAL_CLOSED_EMPTY;
Expand Down Expand Up @@ -12878,6 +12946,7 @@ theorems :=
"REAL_SERIES_RATIO",REAL_SERIES_RATIO;
"REAL_SERIES_RESTRICT",REAL_SERIES_RESTRICT;
"REAL_SERIES_RMUL",REAL_SERIES_RMUL;
"REAL_SERIES_ROOT_TEST",REAL_SERIES_ROOT_TEST;
"REAL_SERIES_SUB",REAL_SERIES_SUB;
"REAL_SERIES_SUBSET",REAL_SERIES_SUBSET;
"REAL_SERIES_SUM",REAL_SERIES_SUM;
Expand Down Expand Up @@ -12952,6 +13021,7 @@ theorems :=
"REAL_SUMMABLE_EQ_COFINITE",REAL_SUMMABLE_EQ_COFINITE;
"REAL_SUMMABLE_EQ_EVENTUALLY",REAL_SUMMABLE_EQ_EVENTUALLY;
"REAL_SUMMABLE_EVEN",REAL_SUMMABLE_EVEN;
"REAL_SUMMABLE_FINITE",REAL_SUMMABLE_FINITE;
"REAL_SUMMABLE_FROM_ELSEWHERE",REAL_SUMMABLE_FROM_ELSEWHERE;
"REAL_SUMMABLE_FROM_ELSEWHERE_EQ",REAL_SUMMABLE_FROM_ELSEWHERE_EQ;
"REAL_SUMMABLE_GP",REAL_SUMMABLE_GP;
Expand All @@ -12966,6 +13036,7 @@ theorems :=
"REAL_SUMMABLE_MUL_RIGHT",REAL_SUMMABLE_MUL_RIGHT;
"REAL_SUMMABLE_NEG",REAL_SUMMABLE_NEG;
"REAL_SUMMABLE_ODD",REAL_SUMMABLE_ODD;
"REAL_SUMMABLE_POS_SUBSET",REAL_SUMMABLE_POS_SUBSET;
"REAL_SUMMABLE_RESTRICT",REAL_SUMMABLE_RESTRICT;
"REAL_SUMMABLE_RMUL",REAL_SUMMABLE_RMUL;
"REAL_SUMMABLE_SUB",REAL_SUMMABLE_SUB;
Expand Down Expand Up @@ -13592,12 +13663,14 @@ theorems :=
"SERIES_LIFT_ABSCONV_IMP_CONV",SERIES_LIFT_ABSCONV_IMP_CONV;
"SERIES_LINEAR",SERIES_LINEAR;
"SERIES_NEG",SERIES_NEG;
"SERIES_NORMCONV_IMP_CONV",SERIES_NORMCONV_IMP_CONV;
"SERIES_ODD",SERIES_ODD;
"SERIES_PASTECART",SERIES_PASTECART;
"SERIES_RATIO",SERIES_RATIO;
"SERIES_REARRANGE",SERIES_REARRANGE;
"SERIES_REARRANGE_EQ",SERIES_REARRANGE_EQ;
"SERIES_RESTRICT",SERIES_RESTRICT;
"SERIES_ROOT_TEST",SERIES_ROOT_TEST;
"SERIES_SUB",SERIES_SUB;
"SERIES_SUBSET",SERIES_SUBSET;
"SERIES_TERMS_TOZERO",SERIES_TERMS_TOZERO;
Expand Down Expand Up @@ -14195,6 +14268,7 @@ theorems :=
"SUMMABLE_EQ_COFINITE",SUMMABLE_EQ_COFINITE;
"SUMMABLE_EQ_EVENTUALLY",SUMMABLE_EQ_EVENTUALLY;
"SUMMABLE_EVEN",SUMMABLE_EVEN;
"SUMMABLE_FINITE",SUMMABLE_FINITE;
"SUMMABLE_FROM_ELSEWHERE",SUMMABLE_FROM_ELSEWHERE;
"SUMMABLE_FROM_ELSEWHERE_EQ",SUMMABLE_FROM_ELSEWHERE_EQ;
"SUMMABLE_GP",SUMMABLE_GP;
Expand Down Expand Up @@ -14379,8 +14453,10 @@ theorems :=
"SUPPORT_EMPTY",SUPPORT_EMPTY;
"SUPPORT_SUBSET",SUPPORT_SUBSET;
"SUPPORT_SUPPORT",SUPPORT_SUPPORT;
"SUP_APPROACH",SUP_APPROACH;
"SUP_CLOSURE",SUP_CLOSURE;
"SUP_EQ",SUP_EQ;
"SUP_EXISTS",SUP_EXISTS;
"SUP_FINITE",SUP_FINITE;
"SUP_FINITE_LEMMA",SUP_FINITE_LEMMA;
"SUP_INSERT",SUP_INSERT;
Expand Down Expand Up @@ -14680,6 +14756,7 @@ theorems :=
"TRIVIAL_LIMIT_AT_NEGINFINITY",TRIVIAL_LIMIT_AT_NEGINFINITY;
"TRIVIAL_LIMIT_AT_POSINFINITY",TRIVIAL_LIMIT_AT_POSINFINITY;
"TRIVIAL_LIMIT_SEQUENTIALLY",TRIVIAL_LIMIT_SEQUENTIALLY;
"TRIVIAL_LIMIT_SEQUENTIALLY_WITHIN",TRIVIAL_LIMIT_SEQUENTIALLY_WITHIN;
"TRIVIAL_LIMIT_WITHIN",TRIVIAL_LIMIT_WITHIN;
"TRIVIAL_LIMIT_WITHINREAL_WITHIN",TRIVIAL_LIMIT_WITHINREAL_WITHIN;
"TRIVIAL_LIMIT_WITHINREAL_WITHINCOMPLEX",TRIVIAL_LIMIT_WITHINREAL_WITHINCOMPLEX;
Expand Down Expand Up @@ -15449,15 +15526,19 @@ theorems :=
"has_derivative",has_derivative;
"has_derivative_at",has_derivative_at;
"has_derivative_within",has_derivative_within;
"has_inf",has_inf;
"has_integral",has_integral;
"has_integral_alt",has_integral_alt;
"has_integral_compact_interval",has_integral_compact_interval;
"has_integral_def",has_integral_def;
"has_liminf",has_liminf;
"has_limsup",has_limsup;
"has_measure",has_measure;
"has_path_integral",has_path_integral;
"has_real_derivative",has_real_derivative;
"has_real_integral",has_real_integral;
"has_real_measure",has_real_measure;
"has_sup",has_sup;
"has_vector_derivative",has_vector_derivative;
"hausdist",hausdist;
"hausdorff_space",hausdorff_space;
Expand Down

0 comments on commit 2430ee0

Please sign in to comment.