HOL html

Files Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _
Theorems Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _

R (theorems)

RAD2_Y_SQRT8
RADIAL_AFF_GE_1_2
RADIAL_AFF_GT_1_2
RADIAL_AFF_GT_3_1
RADIAL_ALT
RADIAL_DIFF
RADIAL_EMPTY
RADIAL_EVENTUALLY_RADIAL
RADIAL_INTERS
RADIAL_LE
RADIAL_NORMBALL
RADIAL_NORM_CO
RADIAL_NORM_LINEAR_INVARIANT
RADIAL_NORM_RADIAL
RADIAL_NORM_YFAN_INTER_BALL
RADIAL_TOPOLOGICAL_COMPONENT_YFAN
RADIAL_UNION
RADIAL_UNIONS
RADIAL_UNIV
RADIAL_VS_RADIAL_NORM
RADIAL_XFAN_INTER_BALL
RADV2
RADV_ETAY
RADV_MONO
RADV_TRANSLATION
RADV_TRANS_EQ
RAD_PI_IMP_WEDGE4
RANK_0
RANK_BOUND
RANK_DIM_IM
RANK_EQ_0
RANK_GRAM
RANK_MUL_LE_LEFT
RANK_MUL_LE_RIGHT
RANK_NULLSPACE
RANK_ROW
RANK_SYLVESTER
RANK_TRANSP
RANK_TRIANGLE
RAT_LEMMA1_SUB
RAWZDIB
RBUTTCS
RCONEGE_INTER_VORONOI_CLOSED_IMP_RCONEGE
RCONE_DISK
RCONE_GE_COS
RCONE_GE_HYPERPLANE
RCONE_GE_INTERS_PROJECTION_KY_LEMMA
RCONE_GE_INTER_VORONOI_CLOSED_PROJECTION_KY_LEMMA
RCONE_GE_SUBSET
RCONE_GE_TRANS
RCONE_GT_CONVEX_HULL_LEMMA
RCONE_GT_EQ_EMPTY_LEMMA
RCONE_GT_HYPERPLANE
RCONE_GT_SCALE
RCONE_GT_SUBSET
RCONE_GT_SUBSET_RCONE_GE
RCONE_LINEAR_INVARIANT
RCONE_PAIR
RCONE_PREP
RDISK_R
RDWKARC
REALLIM_ATREAL_LOCAL
REAL_ABS_INFNORM
REAL_ABS_NORM
REAL_ABS_SUB_INFNORM
REAL_ABS_SUB_NORM
REAL_ABS_TRIANGLE_BOUND
REAL_ADD2_ADD2
REAL_ADD_LE_SUBST_LHS
REAL_ADD_LE_SUBST_RHS
REAL_CONS_IMP_SCALAR_MUL
REAL_CONS_IMP_SUM_CONS
REAL_CONS_STILL_DIFF
REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE
REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE
REAL_CONTINUOUS_ATREAL_IMP_MUL_FUN
REAL_CONTINUOUS_ATREAL_SQRT_COMPOSE
REAL_CONTINUOUS_AT_AZIM_COMPOSE
REAL_CONTINUOUS_AT_AZIM_SHARP
REAL_CONTINUOUS_AT_COMPONENT
REAL_CONTINUOUS_AT_DIHV_COMPOSE
REAL_CONTINUOUS_AT_DOT2
REAL_CONTINUOUS_AT_SQRT_COMPOSE
REAL_CONTINUOUS_IMP_MUL_FUN
REAL_CONTINUOUS_ON_EQ_REAL_CONTINUOUS_AT
REAL_CONTINUOUS_REAL_CONTINUOUS_ATREAL
REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL
REAL_CONTINUOUS_SUB_FUNS
REAL_CONTINUOUS_SUM_FUNS
REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE
REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE
REAL_CONTINUOUS_WITHINREAL_SQRT_COMPOSE
REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE
REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE
REAL_CONTINUOUS_WITHIN_SQRT_COMPOSE
REAL_CONVEX_ON_SECOND_DERIVATIVE
REAL_CONVEX_ON_SECOND_SECANT
REAL_CON_IMP_OPP_FUN_TOO
REAL_CX0
REAL_DIV_GE_1_TACTICS
REAL_DIV_GT_1_TACTICS
REAL_DIV_LE_1
REAL_DIV_LE_1_TACTICS
REAL_DIV_LT_1_TACTICS
REAL_DIV_LZERO
REAL_DIV_NEG
REAL_DIV_SQRT
REAL_EQ_INV
REAL_EQ_RCANCEL_IMP'
REAL_EXISTS_UNIQUE_TRANSABLE
REAL_FINITE_ARGMAX
REAL_FINITE_ARGMIN
REAL_FINITE_MAX_EXISTS
REAL_FINITE_MIN_EXISTS
REAL_GT_IMP_GE
REAL_INTERVAL_Euler_lemma
REAL_INV2
REAL_INV_LT
REAL_LEMMA
REAL_LE_ABS_MUL
REAL_LE_DIV_SIMPLIFY_KY_LEMMA
REAL_LE_LMUL_IMP
REAL_LE_LMUL_LOCAL
REAL_LE_LSQRT
REAL_LE_POW_2
REAL_LE_RDIV_0
REAL_LE_RMUL_IMP
REAL_LE_RSQRT
REAL_LINE_BOUNDED
REAL_LSQRT_LE
REAL_LT_DIV_0
REAL_LT_DIV_NEG
REAL_LT_MUL12
REAL_LT_MUL_3
REAL_LT_ONE_LDIV
REAL_LT_RDIV_0
REAL_LT_RSQRT
REAL_LT_RSQRT2
REAL_LT_SQUARE_POS
REAL_MK_NN_SSQRT
REAL_MK_POS_ABS_'
REAL_MUL_LTIMES
REAL_MUL_LTIMES_LE
REAL_MUL_NN
REAL_MUL_RTIMES
REAL_MUL_RTIMES_LE
REAL_MUL_SUM
REAL_MUL_SUM_NUMSEG
REAL_NEG_LE_RMUL
REAL_NEG_MUL_EQ
REAL_OF_NUM_NOT_EQ
REAL_OPEN_REAL_INTERVAL
REAL_POS_LT_MUL
REAL_POW_2_LE
REAL_POW_2_LT
REAL_POW_NEQ_0
REAL_POW_POW
REAL_PROP_LE_LABS
REAL_PROP_LE_RABS
REAL_PROP_NN_LCANCEL
REAL_PROP_NN_POS
REAL_PROP_NN_RCANCEL
REAL_PROP_NZ_ABS
REAL_RINV_2
REAL_RSQRT_LE
REAL_SSQRT_CHAR
REAL_SSQRT_EQ_0
REAL_SSQRT_MONO
REAL_SSQRT_NEG
REAL_SSQRT_NN
REAL_SSQRT_SQUARE
REAL_SSQRT_SQUARE'
REAL_SUB2_SUB2
REAL_SV_SSQRT_0
REAL_SV_SSQRT_n
REAL_TAYLOR_COS
REAL_TAYLOR_COS_RAW
REAL_WLOG_AAB_SIMPLEX
REAL_WLOG_ABB_SIMPLEX
REAL_WLOG_DS_LEMMA
REAL_WLOG_S3_SIMPLEX
REAL_WLOG_SIMPLEX
REAL_WLOG_SIMPLEX_3d
REAL_WLOG_SIMPLEX_LEMMA
REAL_WLOG_SIMPLEX_LEMMA2
REAL_WLOG_SIMPLEX_LEMMA2_LE
REAL_WLOG_SIMPLEX_SYM
REAL_WLOG_SQUARE2_LEMMA
REAL_WLOG_SQUARE_LEMMA
REDUCE_POINT_FACET
REDUCE_POINT_FACET_EXISTS
REDUCE_WITH_DIV_Euler_lemma
REFL_SYM_0
RELATE_POW2
RELATE_Q_SYS
RELATIVE_INTERIOR_AFFINE_FACE
RELATIVE_INTERIOR_POLYHEDRON_EXPLICIT_ALT
RELATIVE_SUBSET_FCHANGE
REMOVE_DUPLICATES
REMOVE_DUPLICATES_NUM_EMPTY
REMOVE_NEG_AZIM1_SYM_0
REP_CARD_EDGE_SET_FAN
REP_NUMSEG
REP_OF_INVERSE1_SIGMA_FAN
REP_OF_INVERSE1_SIGMA_FAN_IN_D_FAN
REP_VERTEX_3_LOCAL_FAN
RES_DECOMPOSITION
RES_EMPTY
RES_INVERSE
RES_PERMUTES
RES_PERMUTES_DISJOINT_UNIONS
RES_PERMUTES_UNION
RES_RES
RES_RES2
REUHADY
REUHADY1
REVERSE_LINEAR_IMAGE
REVERSE_TABLE
REVERSE_TRANSLATION
RE_CEXP_CX
RE_EQVL_IMP_SYM
RE_EQVL_REFL
RE_EQVL_SCALE1
RE_EQVL_SCALE2
RE_EQVL_SYM
RE_NORM_1
RHO_FUN_DEFORMATION_V3_DEFOR
RHO_IVS_IDD
RHO_LB
RHO_NODE1_INJECTIVE
RHO_NODE1_MONO_WITH_AZIM
RHO_NODE_IS_SUCCESEOR_AZIM
RHO_NODE_K_SY
RHO_NODE_SET_IN_A_PLANE_IMP_POS_DIRECT
RHO_NODE_SY
RHUFIIB
RIGHT_AND_EXISTS_THM
RIGHT_AND_FORALL_TAG
RIGHT_END_POINT
RIGHT_IMP_EXISTS_TAG
RIGHT_IMP_FORALL_TAG
RIGHT_INVERSE_EQUATION
RIGHT_INVERSE_LINEAR
RIGHT_INVERTIBLE_TRANSP
RIGHT_MULT_MAP
RIGHT_OR_EXISTS_THM
RIGHT_OR_FORALL_TAG
RIJRIED
RLXWSTK
ROGERS
ROGERS_AFF_DIM_FULL
ROGERS_EQ
ROGERS_EXPLICIT
ROGERS_EXPLICIT_2
ROGERS_INTER_V_LEMMA
ROGERS_SUBSET_VORONOI_CLOSED
ROTATION_EXISTS
ROTATION_EXISTS_1
ROTATION_LOWDIM_HORIZONTAL
ROTATION_MATRIX_2
ROTATION_MATRIX_EXISTS_BASIS
ROTATION_RIGHTWARD_LINE
ROWS_TRANSP
ROW_IN_F_SY
ROW_SUB
ROW_TRANSP
RRCWNSJ
RRCWNS_WEAK
RSIWAMP
RUNOQPQ
RVFXZBU
RWXUYZZ
RYPDIXT
R_POS_SIN_COS_IDENT
R_SIN_CIRCLE
R_SIN_COS_IDENT
r
r'
r1_ge_fan
r1_ge_is_convex_fan
r1_le_fan
r1_le_is_convex_fan
r2_ge_fan
r2_ge_is_convex_fan
r2_le_fan
r2_le_is_convex_fan
r3_ge_fan
r3_ge_is_convex_fan
r3_le_fan
r3_le_is_convex_fan
r_exists
r_fan
r_fan_is_inter_halfspace
r_is_connected_fan
r_special
rad2_eta2
rad2_x
rad2_x_eta_x
rad2_x_sym
rad2_x_y
rad2_y
rad2_y_e
rad2_y_sym
radV
radial
radial_norm
radial_norm_deprecated
radial_normball
radius
radius_le_circumradius
radius_le_circumradius_all
rank
rat1
rat2
ratform
ratform_add
ratform_div
ratform_inv
ratform_mul
ratform_neg
ratform_pow
ratform_sub
rcone_def_alt
rcone_dot_pos
rcone_eq
rcone_fan
rcone_ge
rcone_gt
rcone_gt_arcV
rcone_gt_arc_triangle
rcone_gt_facet
rcone_hyperplane
rcone_lt
rcone_nz
rcone_refl
rcone_subset_cone
rconesgn
rcons
rduong
re_eqvl
re_eqvl_imp_le
re_eqvl_pos_pos
re_eqvl_real_sgn
real3_exists
real3_minus
real3_neg
real3_of_triple
real3_plus
real3_scale
real_FINITE
real_axis
real_continuous_abs
real_continuous_dih_y_wrt4
real_continuous_dih_y_wrt5
real_continuous_dih_y_wrt6
real_continuous_finite_range_constant
real_continuous_taum
real_interval_contains_0_ball
real_interval_not_sing
real_itv
real_model_008
real_model_3a
real_model_3b
real_model_azim1
real_model_azim2
real_model_azim_c4
real_model_cell23
real_model_cell23_008
real_model_fhbv2
real_model_fhbv2_sym
real_model_g_qxd
real_model_gamma10
real_model_gamma11
real_model_gamma8
real_model_gamma8b
real_model_gamma_qu
real_model_gamma_qx
real_model_gaz4
real_model_gaz6
real_model_gaz9
real_model_gckb
real_model_gr
real_model_ox3q1h_merge
real_model_pema
real_model_pemb
real_model_quqy
real_model_quqy_sym
real_model_sum_azim
real_model_tew
real_model_txq
real_model_ztg4
real_open_contains_real_interval
real_open_delta_y
real_open_empty
real_open_univ
real_open_ups_y
real_periodic_data
real_sub_norm
real_taylor_atn
real_taylor_atn_approx
real_taylor_atn_halfatn4
real_taylor_atn_halfatn4_a
real_taylor_atn_ver1
rect
reduce_exponent
reflection
reflexive
reg
region_conv
regular_spherical_polygon_area
regular_spherical_polygon_area_797
regular_spherical_polygon_area_asnFnhk
relU
remark012_fan
remark01_fan
remark0_fan
remark1_fan
remark3_fan
remark4_fan
remark_fan1
remark_finite_fan1
remark_power_map_points
remove_duplicates2
remove_variable_fan
rep_dartset_leads_into_fan_ds
rep_node_set_fan
reperentation_of_ds2
replace
res
res_inv
res_inverse
reshape
restrict
restricted_hypermap
restriction_cs1_v39
restriction_cs2_v39
restriction_typ1_v39
restriction_typ2_v39
result
retrieve_assum
rev
rev_left_loop
rev_right_loop
rh0
rhand_subset_lhand
rhazim
rhazim2
rhazim2_alt
rhazim2_eq_rhazim3
rhazim2_fan
rhazim2_x
rhazim2_x_div_sqrtdelta_posbranch
rhazim3
rhazim3_alt
rhazim3_eq_rhazim2
rhazim3_fan
rhazim3_x
rhazim3_x_div_sqrtdelta_posbranch
rhazim4
rhazim5
rhazim6
rhazim_fan
rhazim_x
rhazim_x_div_sqrtdelta_posbranch
rho
rho218
rho_alt
rho_bounds
rho_fan
rho_fun
rho_fun_decreasing
rho_ij'
rho_ij'_rho_x
rho_node
rho_node1
rho_rho_fun
rho_sqrtx
rho_x
rho_x_ups_x
rhom
right_commutative
right_distributive
right_id
right_injective
right_inverse
right_loop
right_zero
rjrj
rkkk
rnon_zero
rogers
rogers0
root_lemma
root_th
rot
rot'
rot_bn_rotate
rotate
rotate1
rotate126
rotate2
rotate234
rotate3
rotate345
rotate4
rotate5
rotate6
rotate_min
rotate_to
rotation_about_axis
rotation_dist_decrease
rotation_dist_decrease_lemma
rotation_dist_decrease_special_case
rotation_lemma
rotation_lemma_segments
rotation_lemma_special
rotation_matrix
rotoinversion_matrix
rotr
row
rows
rowvector
rr
rs_sr_unit
rsduong
rsnon_zero
rw_dart_avoids_fan
rw_dart_fan
rw_dart_is_image_set_spherical_coordinate