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 | _ |
U (theorems)
U0_NOT_IN_CONVEX_HULL_FROM_ROGERSU2_IN_AFF_GT
U2_IN_CC_CELL
UAGHHBM
UBHDEUU
UBHDEUU2
UBHDEUU2_hypothesis
UIVNNRR1
UKBRPFE_explicit
ULEKUUB
UNADORNED_NOT_EAR
UNADORNED_OPP
UNBOUNDED_HYPERPLANE
UNIFORMLY_CONTINUOUS_IMP_CONTINUOUS_FAN
UNIFORMLY_CONTINUOUS_ON_ADD_FAN
UNIFORMLY_CONTINUOUS_ON_CMUL_FAN
UNIFORMLY_CONTINUOUS_ON_COMPOSE_FAN
UNIFORMLY_CONTINUOUS_ON_CONST_FAN
UNIFORMLY_CONTINUOUS_ON_ID_FAN
UNIFORMLY_CONTINUOUS_ON_NEG_FAN
UNIFORMLY_CONTINUOUS_ON_SEQUENTIALLY_FAN
UNIFORMLY_CONTINUOUS_ON_SUB_FAN
UNION1_FAN
UNIONS_DELETE
UNIONS_FINITE_LEMMA
UNIONS_IMAGE_FAN_SYM_0
UNIONS_IMAGE_UNIONS
UNIONS_INTER
UNIONS_INTER1
UNIONS_INTERS
UNIONS_SUBSET
UNIONS_TOPOLOGICAL_COMPONENT_EQ_YFAN
UNIONS_UNIONS
UNION_AFF_GE_1_2
UNION_FAN
UNION_SYM_0
UNIQUE1_POINT_FAN
UNIQUE_AZIM_0_POINT_FAN
UNIQUE_AZIM_POINT_FAN
UNIQUE_DARTSET_LEADS_INTO1_FAN
UNIQUE_DARTSET_LEADS_INTO_FAN
UNIQUE_EXISISTING_PROPERTY_C4
UNIQUE_EXISTSENCE_OF_RPHIH
UNIQUE_FOINT_FAN
UNIQUE_ORBIT
UNIQUE_ORDER
UNIQUE_PROPERTY_IN_A_PERIOD
UNIQUE_QY
UNIQUE_QY2
UNIQUE_SIGMA_FAN
UNIQUE_SOLUTION_AFFINE_INDEPENDENT
UNIQUE_SOLUTION_lemma
UNIT_BOUNDED_IN_TOW_FORMS
UNIV_GSPEC
UNI_E_IMP_EE_EQ_SET_OF_EDGE
UNPNFVW
UPFZBZM
UPS_X8_POS
UPS_X_AND_HERON
UPS_X_CONTS_FUNC
UPS_X_EQ_ZERO_COND
UPS_X_POS
UPS_X_POS_SEG
UPS_X_POS_SEG_C
UPS_X_SQUARES
UPS_X_STD_POS
UPS_X_SYM
UPT
UP_TO_4_KY_LEMMA
URRPHBZ1
URRPHBZ2
URRPHBZ3
USEFULL_THHM
UTEOITF
UVGVIXB
UV_IN_AFF2_IMP_TRANSABLE
UV_IN_CONV2
UXCKFPE
UXCKFPE2
U_INTER_U2_FANADD
U_IN_CONV2
u_IN_ORBITS_FAN
u_in_topological_component_yfanadd1
udot_e1_fan
udot_e1_fan1
unadorned_MMs
unadorned_examples
unadorned_v39
unbeta
undiv_gamma3
undiv_gamma3_nn
undup
undup_empty
uni
uni_lemma1
uniformly_continuous_on_fan
union_aff
union_of_cube
union_of_int_cube
unions_cube_subset_ball
unions_lemma
unions_voronoi_center_in_ball_subset_ball
unions_voronoi_subset_ball
uniq
uniq_empty
unique_choice
unique_dart_leads_into
unique_fmap
unique_nmap
unique_tranf_fan
unit0
unit0f
unit6
unobstructed
unzip1
unzip2
upper_dih_hexall_x
upper_dih_x
upper_dih_x_large
upper_dih_x_y
upper_dih_y
upper_dih_y_large
ups_126
ups_x
ups_x_cell3
ups_x_delta_x
ups_x_pos
ups_x_pos24
ups_x_pow2
ups_x_sym
ups_x_triangle_ineq