HOL html

Files Index

Theorems Index

T (theorems)

TAGGED_DIVISION_FINER
TAGGED_DIVISION_OF
TAGGED_DIVISION_OF_ALT
TAGGED_DIVISION_OF_ANOTHER
TAGGED_DIVISION_OF_EMPTY
TAGGED_DIVISION_OF_FINITE
TAGGED_DIVISION_OF_NONTRIVIAL
TAGGED_DIVISION_OF_SELF
TAGGED_DIVISION_OF_TRIVIAL
TAGGED_DIVISION_OF_UNION_SELF
TAGGED_DIVISION_SPLIT_LEFT_INJ
TAGGED_DIVISION_SPLIT_RIGHT_INJ
TAGGED_DIVISION_UNION
TAGGED_DIVISION_UNIONS
TAGGED_DIVISION_UNIONS_EXISTS
TAGGED_DIVISION_UNION_IMAGE_SND
TAGGED_DIVISION_UNION_INTERVAL
TAGGED_PARTIAL_DIVISION_COMMON_POINT_BOUND
TAGGED_PARTIAL_DIVISION_COMMON_TAGS
TAGGED_PARTIAL_DIVISION_OF_SUBSET
TAGGED_PARTIAL_DIVISION_OF_TRIVIAL
TAGGED_PARTIAL_DIVISION_OF_UNION_SELF
TAGGED_PARTIAL_DIVISION_SUBSET
TAG_INVOLUTION
TAG_IN_INTERVAL
TAIL_GUNNER
TANNUMBER_BOUND
TANNUMBER_EVEN
TANNUMBER_HARMONICSUMS
TANPOLY_ODD_EVEN
TAN_0
TAN_ABS_GE_X
TAN_ADD
TAN_ADD_ATN_SIDECOND
TAN_ATN
TAN_BOUND_PI2
TAN_COT
TAN_COT_DOUBLE
TAN_DERIV_POWSER
TAN_DOUBLE
TAN_MONO_LE
TAN_MONO_LE_EQ
TAN_MONO_LT
TAN_MONO_LT_EQ
TAN_NEG
TAN_NPI
TAN_PERIODIC
TAN_PERIODIC_NPI
TAN_PERIODIC_PI
TAN_PI
TAN_PI4
TAN_POS_PI2
TAN_POS_PI2_LE
TAN_POWSER
TAN_POWSER_WEAK
TAN_SEC
TAN_SUB
TAN_TOTAL
TAN_TOTAL_LEMMA
TAN_TOTAL_POS
TARSKI_AXIOM_10_EUCLIDEAN
TARSKI_AXIOM_11_EUCLIDEAN
TARSKI_AXIOM_11_NONEUCLIDEAN
TARSKI_AXIOM_1_EUCLIDEAN
TARSKI_AXIOM_1_NONEUCLIDEAN
TARSKI_AXIOM_2_EUCLIDEAN
TARSKI_AXIOM_2_NONEUCLIDEAN
TARSKI_AXIOM_3_EUCLIDEAN
TARSKI_AXIOM_3_NONEUCLIDEAN
TARSKI_AXIOM_4_EUCLIDEAN
TARSKI_AXIOM_4_NONEUCLIDEAN
TARSKI_AXIOM_5_EUCLIDEAN
TARSKI_AXIOM_5_NONEUCLIDEAN
TARSKI_AXIOM_6_EUCLIDEAN
TARSKI_AXIOM_6_NONEUCLIDEAN
TARSKI_AXIOM_7_EUCLIDEAN
TARSKI_AXIOM_7_NONEUCLIDEAN
TARSKI_AXIOM_8_EUCLIDEAN
TARSKI_AXIOM_8_NONEUCLIDEAN
TARSKI_AXIOM_9_EUCLIDEAN
TARSKI_AXIOM_9_NONEUCLIDEAN
TARSKI_SET
TARSKI_THEOREM
TAUTOLOGY
TAYLOR_CATN
TAYLOR_CCOS
TAYLOR_CCOS_RAW
TAYLOR_CEXP
TAYLOR_CLOG
TAYLOR_CLOG_NEG
TAYLOR_COTXX_BOUND
TAYLOR_COTXX_SQRT_BOUND
TAYLOR_COTX_BOUND
TAYLOR_COT_BOUND
TAYLOR_COT_BOUND_GENERAL
TAYLOR_CSIN
TAYLOR_CSIN_RAW
TAYLOR_EXP
TAYLOR_EXP_WEAK
TAYLOR_LN
TAYLOR_TANX_BOUND
TAYLOR_TANX_SQRT_BOUND
TAYLOR_TAN_BOUND
TAYLOR_TAN_BOUND_GENERAL
TAYLOR_TAN_CONVERGES
TAYLOR_X_COT_CONVERGES
TC_CASES_L
TC_CASES_R
TC_CLOSED
TC_CR
TC_IDEMP
TC_INC
TC_INDUCT_L
TC_INDUCT_R
TC_INV
TC_MONO
TC_RC
TC_REFL
TC_RELPOW
TC_RTC_CASES_L
TC_RTC_CASES_R
TC_RTC_TC_CASES
TC_SC
TC_SYM
TC_TC_RTC_CASES
TC_TRANS
TC_TRANS_L
TC_TRANS_R
TDIV_BOUNDS
TDIV_LE
TELEVISION
TENDSTO_LIM
TENDSTO_REAL
TERM
TERM1
TERMDIFF
TERMDIFF_ALT
TERMDIFF_CONVERGES
TERMDIFF_LEMMA1
TERMDIFF_LEMMA2
TERMDIFF_LEMMA3
TERMDIFF_LEMMA4
TERMDIFF_LEMMA5
TERMDIFF_STRONG
TERMINI_IN_VERTICES
TERMSUBST_ASSIGN
TERMSUBST_EQ
TERMSUBST_FVT
TERMSUBST_NUMERAL
TERMSUBST_TERMSUBST
TERMSUBST_TRIV
TERMSUBST_TRIVIAL
TERMSUBST_TWICE
TERMSUBST_TWICE_GENERAL
TERMVAL_NUMERAL
TERMVAL_TERMSUBST
TERMVAL_VALMOD_OTHER
TERMVAL_VALUATION
TERM_LEMMA1
TERM_LEMMA2
TERM_THM
TERM_UNION
TERM_UNION_NONEW
TERM_UNION_THM
TERM_VALUATION_ITLIST
TERM_VALUATION_VALMOD
TERM_VALUATION_VFREE_IN
TETRAHEDRON_CONGRUENT_EDGES
TETRAHEDRON_CONGRUENT_FACETS
TETRAHEDRON_EDGES
TETRAHEDRON_EDGES_PER_FACE
TETRAHEDRON_EDGES_PER_VERTEX
TETRAHEDRON_VERTICES
THALES
THEOREM
THEOREMS_TRUE
THEOREM_1
THETA_0
THETA_DOUBLE_LEMMA
THETA_LBOUND_1_2
THETA_LE_PSI
THETA_POS
THETA_UBOUND_3_2
THE_DERANGEMENTS_FORMULA
TIETZE
TIETZE_CLOSED_INTERVAL
TIETZE_CLOSED_INTERVAL_1
TIETZE_OPEN_INTERVAL
TIETZE_OPEN_INTERVAL_1
TIETZE_UNBOUNDED
TL
TL_NIL
TL_POLY_CMUL
TL_POLY_EXP_X_SUC
TL_POLY_MUL_X
TOPOLOGICAL_SORT
TOPOLOGY
TOPOLOGY_EQ
TOPOLOGY_UNION
TOPSPACE_EUCLIDEAN
TOPSPACE_EUCLIDEANREAL
TOPSPACE_EUCLIDEANREAL_SUBTOPOLOGY
TOPSPACE_EUCLIDEAN_SUBTOPOLOGY
TOPSPACE_SUBTOPOLOGY
TRACE_0
TRACE_ADD
TRACE_CONJUGATE
TRACE_I
TRACE_MUL_SYM
TRACE_SUB
TRACE_TRANSP
TRAJECTORY_DEFTRAJ
TRANSCENDENTAL_E
TRANSCENDENTAL_LIOUVILLE
TRANSCENDENTAL_MY_TRANSCENDENTAL
TRANSITIVE_STEPWISE_LE
TRANSITIVE_STEPWISE_LE_EQ
TRANSITIVE_STEPWISE_LT
TRANSITIVE_STEPWISE_LT_EQ
TRANSLATION_DIFF
TRANSLATION_EQ_IMP
TRANSLATION_GALOIS
TRANSLATION_UNIV
TRANSP_COLUMNVECTOR
TRANSP_COMPONENT
TRANSP_DIAGONAL_MATRIX
TRANSP_EQ
TRANSP_MAT
TRANSP_MATRIX_ADD
TRANSP_MATRIX_CMUL
TRANSP_MATRIX_NEG
TRANSP_MATRIX_SUB
TRANSP_ROWVECTOR
TRANSP_TRANSP
TRANS_ALT
TRANS_correct
TREAL_ADD_ASSOC
TREAL_ADD_LDISTRIB
TREAL_ADD_LID
TREAL_ADD_LINV
TREAL_ADD_SYM
TREAL_ADD_SYM_EQ
TREAL_ADD_WELLDEF
TREAL_ADD_WELLDEFR
TREAL_EQ_AP
TREAL_EQ_IMP_LE
TREAL_EQ_REFL
TREAL_EQ_SYM
TREAL_EQ_TRANS
TREAL_INV_0
TREAL_INV_WELLDEF
TREAL_LE_ANTISYM
TREAL_LE_LADD_IMP
TREAL_LE_MUL
TREAL_LE_REFL
TREAL_LE_TOTAL
TREAL_LE_TRANS
TREAL_LE_WELLDEF
TREAL_MUL_ASSOC
TREAL_MUL_LID
TREAL_MUL_LINV
TREAL_MUL_SYM
TREAL_MUL_SYM_EQ
TREAL_MUL_WELLDEF
TREAL_MUL_WELLDEFR
TREAL_NEG_WELLDEF
TREAL_OF_NUM_ADD
TREAL_OF_NUM_EQ
TREAL_OF_NUM_LE
TREAL_OF_NUM_MUL
TREAL_OF_NUM_WELLDEF
TREE
TREE_FL
TRIANGLE_ADDITIVE_DECOMPOSITION
TRIANGLE_ANGLE_SUM
TRIANGLE_ANGLE_SUM_LEMMA
TRIANGLE_CONVERGES
TRIANGLE_CONVERGES'
TRIANGLE_DECOMPOSITION
TRIANGLE_FINITE_SUM
TRIANGLE_LEMMA
TRIANGLE_LINEAR_HAS_CHAIN_INTEGRAL
TRIANGLE_PATH_INTEGRALS_CONVEX_PRIMITIVE
TRIANGLE_PATH_INTEGRALS_STARLIKE_PRIMITIVE
TRIANGLE_POINTS_CLOSER
TRIANGULATION_INTER_SIMPLEX
TRIANGULATION_SIMPLICIAL_COMPLEX
TRIANGULATION_SUBSET
TRIANGULATION_UNION
TRIGONOMETRIC_SET_EVEN
TRIGONOMETRIC_SET_MUL_ABSOLUTELY_INTEGRABLE
TRIGONOMETRIC_SET_MUL_INTEGRABLE
TRISECT_60_DEGREES
TRISECT_60_DEGREES_ALGEBRA
TRIVIAL_LIMIT_AT
TRIVIAL_LIMIT_ATREAL
TRIVIAL_LIMIT_AT_INFINITY
TRIVIAL_LIMIT_AT_NEGINFINITY
TRIVIAL_LIMIT_AT_POSINFINITY
TRIVIAL_LIMIT_SEQUENTIALLY
TRIVIAL_LIMIT_WITHIN
TRIVIAL_LIMIT_WITHINREAL_WITHIN
TRIVIAL_LIMIT_WITHINREAL_WITHINCOMPLEX
TRIVIAL_LIMIT_WITHIN_CONVEX
TRIVIAL_LIMIT_WITHIN_REAL
TRIVIAL_LIMIT_WITHIN_REALINTERVAL
TRIV_AND_EXISTS_THM
TRIV_EXISTS_AND_THM
TRIV_EXISTS_IMP_THM
TRIV_FORALL_IMP_THM
TRIV_FORALL_OR_THM
TRIV_OR_FORALL_TAG
TRIV_OR_FORALL_THM
TRUE
TRUE_CLOSURE
TRUE_GENERALIZE
TRUE_NE_FALSE
TRUE_def
TRUONG_1
TRUONG_OPPOSITE_LEMMA
TRUONG_OPPOSITE_THM
TST_ACT
TUBE_LEMMA
TUBE_LEMMA_GEN
TWO
TWOPOW_0
TWOPOW_ABS
TWOPOW_ADD_1
TWOPOW_ADD_INT
TWOPOW_ADD_NUM
TWOPOW_INV
TWOPOW_MK_POS
TWOPOW_NEG
TWOPOW_NZ
TWOPOW_POS
TWOPOW_POW
TWOPOW_SUB_NUM
TYPESET_INHABITED
TYPESET_LEMMA
TYPE_SUBST
Tetralateral_DEF
TriangleCong_DEF
t1
t_thm
tag
tagb
tagged_division_of
tagged_partial_division_of
tailadmissible
tan
tan_def
tannumber
tanpoly
target_edge
target_h
target_set_even
target_set_finite
target_set_odd
target_set_subset
target_v
tau
taut
tautology
tdiv
temma
tends
tends_num_real
tends_real_real
tendsto
tendsto_real
term_CASES
term_INDUCT,term_RECURSION
term_valuation
terminal_adj
terminal_case1
terminal_case2
terminal_case_v
terminal_edge_adj
terminal_edge_bij
terminal_edge_image
terminal_edge_surj
terminal_endpoint
terminal_unique
terminates
termini
termsubst
termval
test_case_int_le_tac
test_ineq_tac
test_real_poly_tac
testform_itlem
th
th0
th1
th1,th2
th2
th3
th_cond
th_set
th_sets
th_vec
thesis
theta
thl
thm
thm2
thm5
thm6
tholds
thr_bij
thr_finite
thread_finite_union
three_delete_size
three_t_enum
three_t_eq
three_t_finite
three_t_not_pair
three_t_not_sing
three_t_size3
three_t_univ
thuv
top2_top
top2_unions
top_closed_unions
top_inter
top_of_metric_empty
top_of_metric_gen
top_of_metric_induced
top_of_metric_inter
top_of_metric_nbd
top_of_metric_open
top_of_metric_open_balls
top_of_metric_top
top_of_metric_union
top_of_metric_unions
top_union
top_unions
top_univ
topology_tybij_th
topspace
toset
totally_bounded_bounded
totally_bounded_cube
totally_bounded_euclid
totally_bounded_pointI
totally_bounded_subset
trace
trajectory
trajform_INDUCT,trajform_RECURSION
trans
transcendental
transitive
transp
transpose2
trap_odd_cell
trap_triple_seg
treal_add
treal_eq
treal_inv
treal_le
treal_mul
treal_neg
treal_of_num
triangle
triangulation
trigonometric_set
trigonometric_set_def
triple_in_comp
triple_par_cell_distinct
trivial
trivial_limit
trivial_lin_combo
true_def
truth
tth
two_endpoint
two_endpoint_segment
two_exclusion
two_two_lemma1
two_two_lemma2
two_two_lemma3
two_two_nine
two_two_union
twopow
twopow_double
twopow_eps
twopow_lt
twopow_pos
type_INDUCT,type_RECURSION
type_bij
type_valuation
typeof
typeset