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)
h_compat_bijh_compat_bij2
h_edge_ball
h_edge_closed_ball
h_edge_closure
h_edge_convex
h_edge_cpoint
h_edge_disj
h_edge_euclid
h_edge_floor
h_edge_inj
h_edge_inter
h_edge_pointI
h_edge_pointIv2
h_edge_row
h_edge_squ_parity
h_edge_subset
h_seg_openball
h_simple_polygonal
h_translate_bij
h_translate_cont
h_translate_h
h_translate_hom
h_translate_inv
h_translate_point
h_translate_v
half_closed
half_closed_above
half_open
half_open_above
half_pos
has_size1
has_size2
has_size2_distinct
has_size2_pair
has_size2_subset
has_size2_subset_ne
has_size3_bij
has_size3_bij2
has_size_bij
has_size_bij2
has_size_bij_set
has_size_drop_le
has_size_insert
has_size_le9
hausdorff_homeomorphsim
hc_edge_closed
hc_edge_convex
hc_edge_inter
hc_edge_pointI
homeo_adj
homeo_adj_eq
homeo_bij
homeo_closed
homeo_closure
homeo_inj
homeo_num_closure
homeo_unions
homeomorphism_compose
homeomorphism_eps_scale
homeomorphism_eps_translate
homeomorphism_induced_top
homeomorphism_inv
homeomorphism_subset
hv_edge
hv_edgeV2
hv_finite_hyper
hv_finite_subset
hv_line_hyper
hv_line_hyper2
hyperplane1_h_translate
hyperplane1_inj
hyperplane1_r_scale
hyperplane1_u_scale
hyperplane1_v_translate
hyperplane2_h_translate
hyperplane2_inj
hyperplane2_r_scale
hyperplane2_u_scale
hyperplane2_v_translate
hyperplane_closed
hyperplane_convex
hyperplane_euclid
hyperplane_ne
hyperplane_scale