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)
RAT_LEMMA1_SUBREAL_ADD_LE_SUBST_LHS
REAL_ADD_LE_SUBST_RHS
REAL_EQ_INV
REAL_EQ_RCANCEL_IMP'
REAL_INV2
REAL_INV_LT
REAL_LE_ABS_MUL
REAL_LT_SQUARE_ABS
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_POW_2_LE
REAL_POW_2_LT
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_SSQRT_CHAR
REAL_SSQRT_EQ_0
REAL_SSQRT_MONO
REAL_SSQRT_NEG
REAL_SSQRT_NN
REAL_SSQRT_SQUARE
REAL_SSQRT_SQUARE'
REAL_SUM_SQUARE_POS
REAL_SV_SSQRT_0
RIGHT_AND_EXISTS_THM
RIGHT_AND_FORALL_TAG
RIGHT_IMP_EXISTS_TAG
RIGHT_IMP_FORALL_TAG
RIGHT_OR_EXISTS_THM
RIGHT_OR_FORALL_TAG
r_scale_bij
r_scale_cont
r_scale_h
r_scale_hom
r_scale_inv
r_scale_point
r_scale_v
real012
real_FINITE
real_div_assoc
real_div_denom
real_div_denom_lt
real_eq_div
real_finite_increase
real_half_EL
real_half_LE
real_half_LLE
real_half_LT
real_middle1_lt
real_middle2_lt
real_sub_half
rectagon_2
rectagon_adj
rectagon_curve
rectagon_delete
rectagon_delete_end
rectagon_endpoint
rectagon_endpoint0
rectagon_graph_k33_false
rectagon_h_edge
rectagon_nonsing
rectagon_order
rectagon_rectangle_grid_sq
rectagon_segment
rectagon_subset
rectagon_subset_endpoint
rectagon_surround_conn2
rectagon_v_edge
rectagonal_graph_k33
rectangle_convex
rectangle_euclid
rectangle_grid_conn2
rectangle_grid_edge
rectangle_grid_h
rectangle_grid_h_conn2
rectangle_grid_sq
rectangle_grid_sq_cls
rectangle_grid_subset
rectangle_grid_v
rectangle_h
rectangle_inter
rectangle_lemma1
rectangle_lemma2
rectangle_lemma3
rectangle_lemma4
rectangle_lemma5
rectangle_lemma6
rectangle_open
rectangle_squ
rectangle_v
reflA_BIJ
reflA_cont
reflA_edge
reflA_h_edge
reflA_homeo
reflA_pointI
reflA_segment
reflA_squ
reflA_v_edge
reflAf_inv
reflAi_inv
reflB_BIJ
reflB_cont
reflB_edge
reflB_h_edge
reflB_homeo
reflB_pointI
reflB_segment
reflB_squ
reflB_v_edge
reflBf_inv
reflBi_inv
reflC_BIJ
reflC_cont
reflC_edge
reflC_homeo
reflC_hv_edge
reflC_pointI
reflC_segment
reflC_squ
reflC_vh_edge
reflCf_inv
reflCi_inv
reflexive
rep3_lt
replace_inj
replace_x
right_left
row_col
row_disj
rthm2