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 | _ |
H (theorems)
H0_LT_SQRT2HAFL_CIRCLE_FORM_LOCAL_FAN
HAFL_CIRCLE_FORM_LOCAL_FAN2
HAFL_CIRCLE_FORM_LOCAL_FAN2_ALT
HAFL_CIRCLE_FORM_LOCAL_FAN_ALT
HALFATN4'
HALFSPACE_EQ
HALFSPACE_EQ_BIS_LE_IMP_HYPERPLANE_EQ_BIS
HALF_CIRCULAR_IN_PLANE
HALF_OF_LE16
HALF_PLANE_CONV
HALP_CIRCLE_IS_INTERSECTION
HAS_MEASURE_AFF_3_INTER_BALL
HAS_MEASURE_AFF_3_UNION_INTER_BALL
HAS_MEASURE_AFF_GT_1_2_INTER_BALL
HAS_MEASURE_XFAN
HAS_MEASURE_XFAN_INTER_BALL
HAS_ORD2_INTERPRET
HAS_ORDERS_IMP_ORBIT_MAP_FIRST_ROW
HAS_ORDK_IN_ORBIT_IMP_SAME_ORBIT
HAS_REAL_DERIVATIVE_CHAIN2
HAS_REAL_DERIVATIVE_LOCAL
HAS_REAL_DERIVATIVE_ZERO_CONSTANT2
HAS_SIZE_2_EXISTS2
HAS_SIZE_6
HAS_SIZE_GE_2
HAS_SIZE_SET_OF_LIST
HAS_SIZE_SET_OF_LIST_4
HAS_SIZE_STDBASIS
HAS_THE_SAME_ORD_LEM
HAVING_ORDERS_K_IMP_CARD_ORBIT_LE_K
HDPLYGY
HDPLYGY_CASE_3
HDPLYGY_CASE_30
HDTFNFZ
HDTFNFZ_ALT
HDTFNFZ_SUBSET
HD_A_CONS
HD_INITIAL_SUBLIST
HD_IN_MCELL
HD_IN_ROGERS
HD_IN_SET_OF_LIST
HD_TRUNCATE_SIMPLEX
HEINE_BOREL_IMP_BOLZANO_WEIERSTRASS_FAN
HEINE_BOREL_LEMMA_FAN
HIJQAHA
HIJ_STEP_1
HJKDESR1a_1cell
HKIRPEP
HKIRPEP_ALT
HL
HL_2
HL_DECREASE
HL_EQ_DIST0
HL_IMP_BARV
HL_LE_SQRT2_IMP_BARV_1
HL_PROPERTIES
HL_TRUNCATE_SIMPLEX_OMEGA_N
HOMOGENEOUS_LINEAR_EQUATIONS_DET
HRXEFDM
HRXEFDM_lemma1
HULL_INTERS_EQ_INTERS
HULL_INTERS_SUBSET_INTERS_HULL
HULL_INTER_EQ_INTER
HULL_INTER_SUBSET_INTER_HULL
HVIHVEC
HVXIKHW
HXHYTIJ
HYP
HYPERFACE_EXISTS
HYPERMAP_INV_MAPS
HYPERMAP_INV_MAPS_ISO_COMM
HYPERMAP_INV_MAPS_ISO_IMAGE
HYPERMAP_MAPS_ISO_COMM
HYPERMAP_MAPS_ISO_IMAGE
HYPERMAP_OF_FAN
HYPERMAP_OF_FAN_ALT
HYPERMAP_OF_FAN_EDGE_NONDEGENERATE
HYPERMAP_OF_FAN_FACE_NODE_INJ
HYPERMAP_OF_FAN_NODE_EQ
HYPERMAP_OF_FAN_NO_DOUBLE_JOINTS
HYPERMAP_OF_FAN_NO_LOOPS
HYPERMAP_OF_LIST
HYPER_MM_COLLINEAR
HYPER_MM_COLLINEAR_TWO_CASES
HYP_ISO_DIH2K_PRESERVED
HYP_ISO_LEMMAA
HYP_LEMMA
HYP_MAPS_INJ
HYP_MAPS_INVS
HYP_elim
HYUAZSE
h0
h0_CSTAB_LT_4
h0_EQ_B_SCS_4I1
h0_EQ_B_SCS_5I1
h0_EQ_B_SCS_5I2
h0_EQ_B_SCS_5M1
h0_EQ_B_SCS_5M2
h0_EQ_B_SCS_6I1
h0_LT_B_SCS_4I1
h0_LT_B_SCS_4I2
h0_LT_B_SCS_4I3
h0_LT_B_SCS_4M6
h0_LT_B_SCS_4M7
h0_LT_B_SCS_4M8
h0_LT_B_SCS_5I1
h0_LT_B_SCS_5I2
h0_LT_B_SCS_5M1
h0_LT_B_SCS_5M2
h0_LT_B_SCS_6I1
h0_LT_B_SCS_6M1
h0_lt_gt
h0_lt_hplus
h0cut
h0cutA
h0cutB
h0cutC
h1
h_b
h_b_IN
h_b_inc
h_b_inj
h_dart
half_def
half_spaces
halfatn
halfatn4
halfatn4_co
halfatn_bounds
halfatn_bounds_abs
halfatn_double
halfatn_half
halfbump_x
halfbump_x1
halfbump_x4
halfbump_x_expand
halfsqrt_ssqrt
hard_case
has
has_bounded_second_derivative
has_measure_ccube
has_measure_cube
has_orders
head
head_on_loop
heading
hinhcau
hinhcau_ball
hinhcau_deprecated
hm0
hmin22
hminus
hminus_cont
hminus_exists
hminus_gt
hminus_h0_hplus
hminus_high
hminus_interval
hminus_lt_h0
hminus_lt_hplus
hminus_prop
hold_def
homog_2x2
homogeneity_thm
hplus
hull_SUBSET
hx
hyp_dart3
hyp_dart4
hyp_dartX
hyp_edge_pairs
hyp_face3
hyp_face4
hyp_face5
hyp_face6
hyp_fan1
hyp_fan2
hyp_fan3
hyp_fan4
hyp_fan5
hyp_fan_tup
hyp_iso
hyp_of_fano
hypermap
hypermap1_of_fanx
hypermap_HYP_elim
hypermap_cyclic
hypermap_eq_lemma
hypermap_lemma
hypermap_of_fan
hypermap_of_fan_rep
hypermap_of_fanx
hypermap_of_list