HOL html

Files Index

Theorems Index

T (theorems)

TABLE
TABLE_4
TAN_HALF
TARJJUW
TAUM_EXTREMAL
TAUM_STD_POS
TAUSTAR_EQ_SYM_0
TAUSTAR_EQ_TAU_STAR_3
TAUSTAR_EQ_TAU_STAR_3_IS_SCS
TAUSTAR_EQ_TAU_STAR_4
TAUSTAR_EQ_TAU_STAR_4_3
TAUSTAR_EQ_TAU_STAR_4_sqrt8
TAUSTAR_EQ_TAU_STAR_5
TAUSTAR_EQ_TAU_STAR_5_pro_cs
TAUSTAR_EQ_TAU_STAR_5_sqrt8
TAUSTAR_EQ_TAU_STAR_6
TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_4
TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_5
TAUSTAR_EQ_TAU_STAR_IS_SCS_CASE_6
TAUSTAR_LE_0_XWNHLMD
TAUSTAR_LE_TAUSTAR_TRANSFER
TAUSTAR_V3_DEFOR
TAUSTAR_V3_DEFOR_MK
TAUSTAR_V3_DEFOR_MK_TWO_CASES
TAUSTAR_V3_DEFOR_TWO_CASES
TAUSTAR_WW_DEFOR
TAU_FUN_LE
TAU_STAR_COVER
TAU_STAR_POS
TAYLOR_SIN
TBRMXRZ1
TBRMXRZ2
TDHUFHCYVHYBCC
TECOXBM
TECOXBM1
TECOXBM2
TECOXBMv2
TEST
TEWNSCJ_MERGED
TEZFFSK
TFITSKC
TFITSKCv1
THANG_DEU
THEOREM_RE_AFF_LT31
THETA_BOUNDS
THE_SLICING_INTO_2_LEMMA
THIRD_CHAIN_GENERAL
THREAD_IF
THREE_LE_CC_CARD
THREE_MOD_CONSECUTIVES
THREE_NOT_COLL_DETER_PLANE
THREE_POINTS_COP
THREE_POINT_IMP_EXISTS_3
THREE_POS_IMP_DIHV_STABLE
TIEEBHT
TIWWFYQ
TOW_BIJS_IMP_BIJ_BETWEEN_FIRST
TOW_DISTINCT_POINTS_EXISTS_RD_NOT_COLLINEAR
TOW_NON_VEC0_IMP_NOT_REFL_POLAR_LT
TOW_NON_VEC0_POLAR_LE_IMP_NOT_LT
TOW_POINTS_IN_IMP_AFF_GT_SUBSET
TOW_REAL_EXISTS_COMBINED
TO_LIN_F
TO_LIN_F0
TO_LIN_F1
TO_UYCH
TRACE_0
TRACE_ADD
TRACE_I
TRACE_MUL_SYM
TRACE_SUB
TRANF
TRANSFER_SUBSET_BB
TRANSLATE_AFFINE_KY_LEMMA1
TRANSP_COLUMNVECTOR
TRANSP_COMPONENT
TRANSP_EQ
TRANSP_MAT
TRANSP_MATRIX_ADD
TRANSP_MATRIX_CMUL
TRANSP_MATRIX_NEG
TRANSP_MATRIX_SUB
TRANSP_ROWVECTOR
TRANSP_TRANSP
TRANSTER_IS_UNADORNED
TRANS_BBINDEX_ID
TRANS_BBINDEX_MIN_EQ
TRANS_BBPRIME2_SUBSET
TRANS_DIAG
TRANS_E
TRANS_FF
TRANS_ID_INDEX
TRANS_IMAGE_BBINDEX_EQ
TRANS_MMS_SUBSET
TRANS_MOD_EQ
TRANS_MOD_EQ_SUC
TRANS_PROPERTY
TRANS_PROPERTY_IN
TRANS_SCS_AM_ID
TRANS_SCS_AM_ID_MOD
TRANS_SCS_A_ID
TRANS_SCS_A_ID_MOD
TRANS_SCS_BBPRIME
TRANS_SCS_BM_ID
TRANS_SCS_BM_ID_MOD
TRANS_SCS_B_ID
TRANS_SCS_B_ID_MOD
TRANS_SCS_HI_ID
TRANS_SCS_J_ID
TRANS_SCS_J_ID_MOD
TRANS_SCS_LO_ID
TRANS_SCS_STR_ID
TRANS_SCS_WW_ID
TRANS_SUC_IMP_INCREASE
TRANS_V
TRAN_COMMUTATIVE_F1_FAN
TRAN_COMMUTATIVE_F1_FAN0
TRAN_COMMUTATIVE_F1_FAN1
TRAN_COMMUTATIVE_F1_FAN2
TRAN_COMMUTATIVE_F1_FAN3
TRAN_COMMUTATIVE_F1_FAN_POWER
TRAN_COMMUTATIVE_F1_FAN_POWER1
TRAN_COMMUTATIVE_F1_FAN_POWER2
TRAN_COMMUTATIVE_F1_FAN_POWER3
TRAN_IN_TRANF
TRIANGLE_IN_BARRIER
TRIANGLE_IN_BARRIER'
TRIANGLE_IN_STRICT_QUA
TRIANGULAR_FACE
TRIANGULAR_FACE_AZIM_DART_BOUNDS
TRIVIAL_LIMIT_AT_FAN
TRIVIAL_LIMIT_AT_INFINITY_FAN
TRIVIAL_LIMIT_SEQUENTIALLY_FAN
TRIVIAL_LIMIT_WITHIN_FAN
TRIVIVAL_LE
TRIV_AND_EXISTS_THM
TRIV_EXISTS_IMP_THM
TRIV_FORALL_IMP_THM
TRIV_OR_FORALL_TAG
TRI_LEMMA
TRI_SQUARES_BOUNDS
TRI_STABLE_K_EQ_3
TRI_UPS_X_POS
TRI_UPS_X_SQRT
TRI_UPS_X_SQUARES
TRI_UPS_X_STRICT_POS
TRUNCATE_0_EQ_HEAD
TRUNCATE_SIMPLEX
TRUNCATE_SIMPLEX0
TRUNCATE_SIMPLEX_ADD1
TRUNCATE_SIMPLEX_ADD1_ALT
TRUNCATE_SIMPLEX_BARV
TRUNCATE_SIMPLEX_CONS
TRUNCATE_SIMPLEX_EQ_BUTLAST
TRUNCATE_SIMPLEX_EXISTS
TRUNCATE_SIMPLEX_EXPLICIT
TRUNCATE_SIMPLEX_EXPLICIT_0
TRUNCATE_SIMPLEX_EXPLICIT_1
TRUNCATE_SIMPLEX_EXPLICIT_2
TRUNCATE_SIMPLEX_EXPLICIT_3
TRUNCATE_SIMPLEX_GENERAL_0
TRUNCATE_SIMPLEX_GENERAL_1
TRUNCATE_SIMPLEX_GENERAL_2
TRUNCATE_SIMPLEX_INITIAL_SUBLIST
TRUNCATE_SIMPLEX_PROP
TRUNCATE_SIMPLEX_REFL
TRUNCATE_SIMPLEX_SUBSET
TRUNCATE_SIMPLEX_UNIQUE
TRUNCATE_TRUNCATE_SIMPLEX
TRUONGG
TRUONG_1
TRUONG_LEMMA
TRUONG_WELL
TSKAJXY
TSKAJXY_1
TSKAJXY_2
TSKAJXY_DERIVED4
TSKAJXY_HYPa
TSKAJXY_statement
TSKAJXY_statement_special_case
TUAPYYU
TUAPYYU1
TUAPYYU_IMP_CASES
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
TWO_DIAGONAL_AT_MOST
TWO_DIAGONAL_AT_MOST1
TWO_EQ_IMP_COL3
TWO_EQ_SYSTEM_THM
TWO_IMP_HAS_SIZE_GE_2
TWO_NON_ZERO_VECS_NOT_EQ_EQ_PLT
TWO_NOT_EQ_VECS_SUM_ARG_DIFF_TWO_PI
TWO_PI_POS
TWO_REARRANGEMENT_LEMMA
TWO_REARRANGEMENT_LEMMA_ALT
TWO_SIDES_SUCESSIVE
TWO_UNIT_ORTH_VECTORS_IMP_ORTHONORMAL
TXDIACY
TXFBALB
TXFBALB_VERSION
TXIWYHI
TXQTPVC_MERGED
TYUNJLA
t0
table_multiplier
tagb
tail_on_loop
take
tam
tam1
tam2
tame_1
tame_10
tame_11
tame_11a
tame_11b
tame_12
tame_12o
tame_13
tame_13a
tame_2
tame_3
tame_4
tame_5
tame_5a
tame_6
tame_7
tame_8
tame_9
tame_9a
tame_hypermap
tame_opposite_hypermap
tame_table_d
tame_table_d_values
tan_one_one
tau0
tau0_not_zero
tau3
tau3_azim
tau3_sym
tau3_taum
tau3_taum_40
tau3_taum_d
tau3_taum_dfun
tau3_taum_nonplanar
tauV
tauVEF
tauVEF_EQ_taum
tauVEF_alt1
tauVEF_alt2
tauVEF_tau_fun
tau_fan
tau_fun
tau_fun_azim
tau_lowform_x
tau_lowform_x_alt
tau_m_diff_quotient
tau_m_diff_quotient2
tau_residual_x
tau_star
tau_x_tau_residual_x
tau_x_tau_residual_x_general
taud
taud_053
taud_2h0
taud_D1_num_x
taud_D2_num_x
taud_continuous
taud_ge_flat_term
taud_minimizer
taud_minimizer_cases
taud_minimizer_terminal_hex_cases
taud_minimizer_terminal_pent_cases
taud_mu_clauses
taud_mud_126_x
taud_mud_135_x
taud_sqrt20
taud_v4_D2_num
taud_x
taud_x_ALT
taud_x_taud
taum
taum_123
taum_1flat_x
taum_1flat_x_alt
taum_2flat_x
taum_2flat_x_alt
taum_3flat_x
taum_3flat_x_alt
taum_attains_inf
taum_compose_xrr
taum_dih_y
taum_hexall_x
taum_sub156_x
taum_sub1_x
taum_sub246_x
taum_sub345_x
taum_sym
taum_sym_cases2
taum_taum_x
taum_template_B_x
taum_x
taum_x1
taum_x1_x2
taum_x2
taum_y1
taum_y1_y2
taum_y2
taumin
tauq
tauq_x_y
taustar3
taustar3_fun
taustar_taum
taustar_taum_dfun
taustar_v39
taylor_acs
taylor_atn
taylor_coeff0
taylor_coeff_catn
taylor_coeff_catn0
taylor_coeff_catn1
taylor_coeff_catn_deriv
taylor_coeff_catn_pos
taylor_error_bound
taylor_interval
taylor_inv
taylor_series_inv_pow
taylor_sqrt
term_bound
terminal_hex_126_reduction
terminal_hex_135_reduction
terminal_hex_234_reduction
terminal_pent_tau126_2
terminal_pent_tau126_2h0
terminal_pent_tau126_delta20
terminal_pent_tau135_012
terminal_pent_tau135_2
terminal_pent_taum
terminal_pent_taum126_012
terminal_pent_taum2
terminal_quad_lemma
terminal_std_ear_jnull_empty
terminal_std_tri_1080462150_empty
terminal_std_tri_2200527225_empty
terminal_std_tri_2739661360_empty
terminal_std_tri_2900061606_empty
terminal_std_tri_3106201101_empty
terminal_std_tri_4143829594_empty
terminal_std_tri_4922521904_empty
terminal_std_tri_7097350062a_empty
terminal_std_tri_7459553847_empty
terminal_std_tri_7645170609_empty
terminal_std_tri_7881254908_empty
terminal_std_tri_9816718044_empty
terminal_std_tri_OMKYNLT_1_2_empty
terminal_std_tri_OMKYNLT_2_1_empty
terminal_std_tri_ear_stab_empty
terminal_tri_5405130650_empty
test_aug9_2011
test_domain_xi
test_ineq_tac
test_real_poly_tac
tf_compose
tf_delta4_squared_x
tf_delta_x
tf_delta_x4
tf_dih2_x
tf_dih3_x
tf_dih4_x
tf_dih5_x
tf_dih6_x
tf_dih_x
tf_ldih2_x
tf_ldih3_x
tf_ldih5_x
tf_ldih6_x
tf_ldih_x
tf_lfun_sqrtx1_div2
tf_plus
tf_product
tf_rad2_x
tf_scale
tf_sol_x
tf_uni
tf_unit
tf_vol_x
tf_x1
tf_x2
tf_x3
tf_x4
tf_x5
tf_x6
tf_y1
tf_y2
tf_y3
tf_y4
tf_y5
tf_y6
tgt
tgt_exact
tgt_interval
th
th0
th1
th2
th3
th3a
th3a12
th3b
th3b1
th3c
th3d
th4
th_T
th_imp
th_set
th_sets
th_vec
the
the_SAME_orbit_exceptional
the_SAME_orbit_face
the_SAME_orbit_quadrilaterals
the_SAME_orbit_triangles
the_SAME_type
the_some
them1
them2
them3
them4
them5
them6
them7
them8
theoremmm
there_exists_component_contain_aff_gt_fan
thm
thm1
thm2
thm3
thm4
thm5
thm6
to_head
top
topological_component_subset_yfan
topological_component_yfan
torsor
total_solid
total_weight
tpx
tpy
tr5
tr6
tr_fun
tr_set
trace
tran
tran_in_dart_newfan
tranf
tranf_eq_image_of_tran
trans
trans_normball
trans_strech_trans_radial
transfer_v39
transitive
transp
trg_boolset
trg_d3_sym
trg_dist3_sym
trg_in_union
trg_setbool
trg_sub_bo
trg_sub_se
tri_itv
tri_stable
tri_sy_explicit
tri_sy_lemma
triangle
triangle_area_lower_bound
triangle_height_lemma
triangle_of_node
triangle_set_of_node
triangles
triangles_set
trip_eq
triple_of_real3
triv2
triv_ch
trivial_limit_fan
trivial_ratform
trn_fun
tru_pack
truncate_dih_x
truncate_dih_x_dih_x
truncate_dih_x_sym
truncate_dih_x_sym2
truncate_gamma23_x
truncate_gamma23_x_B
truncate_gamma23_x_C
truncate_gamma23a_x
truncate_gamma2_x
truncate_gamma3f_x
truncate_set_of_list
truncate_sol_x
truncate_sol_x_sol_x
truncate_sqrt
truncate_sqrt_le
truncate_vol3f
truncate_vol3r_456
truncate_vol_x
truncated_packing
truncated_path_lemma
tsk_lemma1
tuple_opposite_hypermap
two6
twopow
twopow_eps
type150
type_of_node