HOL html

Files Index

Theorems Index

P (theorems)

PAATDXJ
PACKING
PACKING_BALL_BOUNDARY
PACKING_CHAPTER_MAIN_CONCLUSION
PACKING_IMP_CLOSED
PACKING_IMP_DISCRETE
PACKING_INSERT
PACKING_SUBSET
PACKING_TRANS
PACK_INEQ_DEF_A_797
PAHFWSI
PAIRWISE_ORTHOGONAL_IMP_FINITE
PAIRWISE_ORTHOGONAL_INDEPENDENT
PAIR_D3
PAIR_DIST
PAIR_FUN_SYM_0
PAIR_IN_DART1_OF_FAN
PAIR_IN_DART1_OF_FAN_IMP_NOT_EQ
PAIR_IN_DART_OF_FAN
PAIR_LEMMA
PARALLELOGRAM_LAW
PARALLEL_PROJECTION
PASTECART_ADD
PASTECART_CMUL
PASTECART_EQ_VEC
PASTECART_NEG
PASTECART_SUB
PASTECART_VEC
PASTECART_VSUM
PCRTTID
PDPFQUK
PEDSLGV1
PEDSLGV2
PERIODIC_AT0_IMP_ANY
PERIODIC_EQ_IMAGE
PERIODIC_IMAGE
PERIODIC_IMAGE2
PERIODIC_IMAGE_EQUAL
PERIODIC_INJ_MOD
PERIODIC_PROPERTY
PERIODIC_PSORT
PERIODIC_REDUCE_MOD
PERIODIC_RHO_NODE1
PERMUTES_COMPOSITION
PERMUTES_IMP_INSIDE
PERMUTES_IMP_RES_EQ_FUN
PERMUTES_TRIVIAL
PERMUTES_a_PERMUTES_b
PERMUTE_BARV3
PEROPP_IN_BB_SYM_0
PERPENCULAR_PART_IDENT0
PER_COEF1
PER_COEF1_COEF2
PER_COEF1_COEF3
PER_COEF1_WITH_COEF2
PER_COEF1_WITH_COEF3
PER_COEF1_WITH_COEF4
PGSQVBL
PHAN_TICH
PI2_EQ_ACS0
PIIJBJK
PITHAGOR_CROSS
PITHAGOR_NORM
PITHAGO_THEOREM
PI_APPROX
PI_APPROX_4
PI_EST
PI_EST2
PI_LOWERBOUND_WEAK
PI_SER
PI_TO_TWO_PI_NEG_SIN
PJFAYXI
PLAIN_HYPERMAP
PLAIN_HYPERMAP_OF_FAN
PLANE_AFFINE_HULL_3
PLANE_AFFINE_HUL_INTER_P
PLANE_IMP_AFFINE
PLANE_NORM_IMP_AFFINE
PL_ANGLE_PROPERTY
PMAT1_EQ_SY
PMAT1_EQ_SY_P
PMAT2_EQ_SY
POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR
POINTS_IN_BALL_ANNULUS_NOT_COLLINEAR2
POINTS_IN_HAFL_CIRCLE
POINT_COM_AFF_GT_INTER
POINT_IN_AFF_GE_IMP_IN_EDGE
POINT_IN_AFF_LT_SYM_0
POINT_IN_BBS_IS_NOT_0_3
POINT_IN_CLOSURE_AFF_GT_1_2
POINT_IN_LINE
POINT_IN_LINE1
POINT_PRESENTED_IN_RHOND1
POLAR_CYCLIC_FUN_IMP_ALL_BELONG
POLAR_LE_NOT_VEC0_IMP_PL_ANG_LE
POLAR_LE_REFL_EQ
POLAR_LT_IMP_NOT_EQ
POLAR_LT_TRANS
POLAR_MONOPOLY_IN_FIRST_ITERVAL
POLFLZY
POLYHEDRON_BIS
POLYHEDRON_CONFORMING_FAN
POLYHEDRON_D1_D
POLYHEDRON_FACET_SUM_4Pi
POLYHEDRON_FAN
POLYHEDRON_MEMBER
POLYHEDRON_NODE_3
POLYHEDRON_PLAIN
POLYHEDRON_TGJISOK
POLYHEDRON_VORONOI_CLOSED
POLYHEDRON_VORONOI_LIST
POLYSORT_BIJ2
POLYTOPE_FAN80
POLYTOPE_VORONOI_CLOSED
POLYTOPE_VORONOI_LIST
POLYTOPE_VORONOI_LIST_BARV
POLY_F_APPEND
POLY_F_EVEN_ALT
POLY_F_EVEN_APPEND
POLY_F_ODD_APPEND
POLY_F_SING
POLY_SORT
POLY_SORT_BIJ
POLY_SORT_LEMMA
POS_COMPATIBLE_WITH_ATN2
POS_EQ_INV_POS
POS_EQ_NOT_COPLANANR
POW2_1_BOUNDED
POW2_EQ_0
POWER
POWER_0
POWER_1
POWER_2
POWER_FF_HYP_ID
POWER_FF_HYP_ID1
POWER_FF_OF_HYP_EQ
POWER_FF_OF_HYP_EQ1
POWER_FUNCTION
POWER_IN_LEMMA
POWER_MOD_FUN
POWER_RHO_NODE_SY
POWER_RIGHT
POWER_SND
POWER_TO_ITER
POW_1
POW_2
POW_2_LT
POW_MINUS1
PPBTYDQ
PPHEUFG
PPx
PQCSXWG1
PQCSXWG1_SYM
PQCSXWG2
PQCSXWG2_ATREAL
PQCSXWG2_WITHINREAL
PR23_OF_D1_FAN
PR23_OF_D20_FAN
PREIMAGE_BIJ
PRESERABLE_AFF_GE_SUBSET
PRESERVES_NORM_INJECTIVE
PRESERVES_NORM_PRESERVES_DOT
PREV_EL
PREV_EL_ALT
PREV_EL_LIST_PAIRS
PREV_EL_LIST_PAIRS_GENERAL
PREV_NEXT_ID
PRE_0
PRE_B1_0
PRE_HE
PRE_HER
PRE_INVERSE_SUB
PRE_IPVICGW
PRE_IVS_RHO_NODE1_DETE
PRE_NUM
PRE_RADV_COND
PRE_TRIG_FORM_VEC2
PRIOR_TO_LESS_THAN_PI_LEMMA
PRIOR_TO_LESS_THAN_PI_LEMMA_ALT
PRODUCT_1
PRODUCT_2
PRODUCT_3
PRODUCT_PERMUTE
PRODUCT_PERMUTE_NUMSEG
PROD_ABS
PROD_CMUL
PROD_EQ
PROD_MUL
PROD_POS
PROD_POS_GEN
PROD_TWO
PROD_ZERO
PROJECTION_0
PROJECTION_DIST2
PROJECTION_DIST_SPECIAL_EQ
PROJECTION_DIST_SPECIAL_LE
PROJECTION_LINEAR
PROJECTION_NEG
PROJECTION_ORTHOGONAL
PROJECTION_SUB
PROJECTION_SUM_DIST
PROJECTION_VEC0
PROJECTION_ZERO
PROJECTOR_NOT_EQ_VEC0
PROJECT_EQ_VEC0_IMP_PARALLED
PROJEC_EQ_0_IFF_COLL
PROPERTIES_AFF_GT_SUBSET_WEDGE
PROPERTIES_EAR_SY
PROPERTIES_GENERIC
PROPERTIES_GENERIC1
PROPERTIES_GENERIC_LOCAL_FAN
PROPERTIES_GENERIC_LOCAL_FAN_ALT
PROPERTIES_OF_FAN_IN_B_SY
PROPERTIES_OF_IVS_AZIM_CYCLE2
PROPERTIES_TRIANGLE_FAN
PROPERTIES_TRIANGLE_FAN_lemma1
PROPERTIES_TRIANGLE_FAN_lemma2
PROPERTY_OF_K_SCS
PROP_EQU_EQ_BB
PROP_EQU_EQ_BBPRIME
PROP_EQU_IS_SCS
PROP_OPP_4M8_13
PROP_OPP_DIAG_4I3_13
PROP_OPP_DIAG_4M2_13
PROP_OPP_DIAG_4M3_13
PROP_OPP_DIAG_4M5_13
PROP_OPP_DIAG_4M6_13
PROP_OPP_DIAG_4M8_13
PROP_OPP_DIAG_5M1_02
PROP_OPP_DIAG_5M1_03
PROP_OPP_DIAG_5M3_02
PROP_OPP_DIAG_5M3_03
PROVE_B1B2_POS
PROVE_DELTA_OVER_SQRT_2UPS
PROVE_DIST_FROM_V1
PROVE_EQ_DIST_FROM4
PROVE_EXISTING_MAX_IN_CYCLIC_FINITE_SET
PROVE_EXISTS_CIR_OF_FOUR_POINTS
PROVE_EXISTS_H_DELTA_0
PROVE_EXISTS_RADV
PROVE_IN_AFFINE_HULL_4
PROVE_MIN_ELEMENT_IN_FINITE_CYCLIC_SET
PROVE_NOT_COLLINEAR
PROVE_POS_THINGS
PROVE_P_LE
PROVE_SIN_LE
PROVE_SLICING_FAN
PROVE_THE_HYPOTHESI_FOR_74
PROVE_THE_SLICE_ASSUMPTION
PROVE_UNION_AFF22_SUBSET
PROVE_XISTS_MAX_ELEMENT_LT_P
PRO_ADD_NOT_IN_SCS_M
PRO_EQU_DSV_EQ
PRO_EQU_ID
PRO_EQU_ID1
PRO_EQU_IS_EAR
PRO_EQU_TAUSTAR_EQ
PRO_EXP
PSORT_5_EXPLICIT
PSORT_EQ_SYM
PSORT_EQ_SYM1
PSORT_MOD
PSORT_PERIODIC
PVLJZLA
PWEIWBZ
PWVIIOL
PYTHAGORAS_PROJECTION
p
pack_ineq_def_a
packing
packing_lt
packing_subset_unions_ball
packing_trg
pad2d3d_SUB
pad2d3d_dot_v
pad2d3d_dropout
pad2d3d_dropout_lemma
pad2d3d_facet
pad_in
pair_disjoint_f10_f20_f30
pairmap
parallel
part0
part1
part2
part3
part4
part5
part6
part7
part8
partial
partial2
partial_pow
partition_DEF
partition_components
partition_orbit
pathL
pathL_bound
pathL_pathR
pathR
pathR_bound
pcancel
pcomp
per
perimeter
perimeterbound
periodic
periodic2
periodic2_MOD
periodic2_SUC_periodic
periodic2_cs_adj
periodic2_funlist
periodic2_funlistA
periodic2_mod_reduce
periodic2_mod_sym_reduce
periodic_empty
periodic_fn
periodic_mod
periodic_mod_reduce
periodic_mult
periodic_nk
periodic_numseg
periodic_o
periodic_shift
periodic_sum
periodic_sum_shift
periodic_vv_inj
perm_eq
perm_eq_bn_cong_iso
permuters_of_enf_fan
permutes_4points_collinear
permutes_4points_collinear1
permutes_ID_ab
permutes_sigma_fan
peropp
peropp2
peropp_periodic
phi
phi_domain
phi_domain_inf
phi_fun
phi_fun'
phin
phin_ONTO
phivo
pi2_sub_atn2
pi_atn
pi_interval
pi_rt18
pl_angle
place_there_point_line_fan
plain_hypermap
plain_hypermap_edge
plain_hypermap_fan
plain_op_lm
planar_deform_dist
planar_hypermap
planar_ind
plane
plane_3p
plane_norm
pmat1
pmat2
pmp_to_iter
point_eq
point_in_aff_ge
point_in_aff_ge_1_1
point_in_aff_gt_2_1_change_point_in_aff_gt_1_2
point_in_aff_gt_in_yfan
point_in_yfan_and_point_in_xfan_indepent_fan
point_in_yfan_is_not_inv_fan
point_in_yfan_not_x_fan
points_in_aff_ge_0_2
polar_angle
polar_c
polar_cycle
polar_cycle_on
polar_le
polar_lt
poly_f
poly_f_even
poly_f_odd
poly_sort_antisym
poly_sort_fn
poly_sort_trans
polyhedron_3_facets
polyhedron_edge_sum
polyhedron_sum_sum_edge
pos1
pos2
pos_imp_scs_arrow_empty
pos_in_aff_ge_fan
pos_in_aff_gt_2_1_fan
pos_in_aff_gt_fan
pos_lemma
pos_vector_angle_bounds
pow1
pow2
pow3
pow3_identity
pow4
pow_g
pow_lesthan_1
pow_lesthan_eq_1
pow_node_fan
pow_parity
pow_sigma_0
pow_sigma_1
pow_sigma_fan
power_fun_in_domain
power_inverse_element_lemma
power_list
power_map_fix_point
power_map_fix_set
power_map_points
power_map_points_edge_fan
power_maps
power_n_fan
power_permutation
power_permutation_outside_domain
power_power_relation
power_res_face_map
power_th
power_unit_map
pr1
pr2
pr23
pr23_inj_in_dfan
pr3
pr4
pre_beta
pre_def1_4_3b
pre_def_4_3b_alt
pre_quarter_oct
pred0
pred1
predC
predD
predD1
predI
predT
predU
preim
preimage
prev_el
prev_hd_th
primitive
prod
prod_DEF
prod_EXISTS
product_3
profile_apex4_d
profile_apex5_d
profile_std56_flat_free_d
proj_point
proj_x1
proj_x2
proj_x3
proj_x4
proj_x5
proj_x6
proj_y1
proj_y2
proj_y3
proj_y4
proj_y5
proj_y6
projection
projection_lemma
projection_proj_point
projection_scale
promote
promote1_to_6
promote3_to_6
promote_pow2
promote_pow3
properties12_fan7
properties1_inside_fan
properties1_of_fan7
properties_coordinate
properties_edges_eq_fan
properties_fully_surrounded
properties_inside_collinear0_fan
properties_inside_collinear1_fan
properties_inside_collinear_fan
properties_of_collinear4_points_fan
properties_of_coplanar
properties_of_cyclic_set
properties_of_elements_in_face_fan
properties_of_elements_in_face_fully_surroundedfan
properties_of_elements_in_node_fully_surroundedfan
properties_of_f1_fan
properties_of_fan7
properties_of_fully_surrounded1_fan
properties_of_graph
properties_of_graph1
properties_of_set_of_edge
properties_of_set_of_edge_fan
property_of_cyclic_set
property_of_cyclic_set1
property_of_cyclic_set2
property_of_cyclic_set3
prove
psort
psort_4
psort_5
psort_inj
psort_mod
psort_sym
pth
pth1
pth_zero
pthm