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 | _ |
P (theorems)
PAIR_LEMMAPAIR_LEMMAv2
PAIR_SPLIT
PI_EST
PI_EST2
PI_SER
PROD_ABS
PROD_CMUL
PROD_EQ
PROD_MUL
PROD_POS
PROD_POS_GEN
PROD_TWO
PROD_ZERO
p_connA
p_conn_ball
p_conn_conn
p_conn_diff
p_conn_euclid
p_conn_hv_finite
p_conn_open
p_conn_subset
pair_apply
pair_indistinct
pair_order_endpoint
pair_size_2
pair_swap
pair_swap_adj
pair_swap_invol
pair_swap_pair
pair_swap_unique
par_cell_cell
par_cell_cell_partition
par_cell_closure
par_cell_closure_cell
par_cell_comp
par_cell_curve_cell_disj
par_cell_curve_disj
par_cell_disjoint
par_cell_even_imp
par_cell_h
par_cell_h_in_rectangle
par_cell_h_rectangle
par_cell_h_squ
par_cell_nbd
par_cell_nonempty
par_cell_odd_imp
par_cell_open
par_cell_partition
par_cell_point
par_cell_pointI
par_cell_pointI_trichot
par_cell_point_h
par_cell_point_in_rectangle
par_cell_point_rectangle
par_cell_point_v
par_cell_simple_arc
par_cell_squ
par_cell_squ_neg
par_cell_squ_rectangle
par_cell_union_comp
par_cell_union_disjoint
par_cell_unions_nonempty
par_cell_v
par_cell_v_in_rectangle
par_cell_v_rectangle
par_cell_v_squ
parity
parity_even_cell
parity_h
parity_point
parity_squ
parity_union
parity_union_triple
parity_union_triple_even
parity_union_triple_odd
parity_unique
parity_v
part0
part1
part2
part3
part4
part5
part6
part7
part_below_finite
part_below_h
part_below_subset
part_below_v
partition_DEF
path_component_in
path_component_subspace
path_domain
path_eq_conn
path_refl
path_symm
path_symm_eq
path_trans
pconn_refl
pconn_symm
pconn_trans
pi_bounds
planar_graph_hv
planar_graph_rectagonal
planar_is_graph
planar_iso
plane_graph_contain
plane_graph_image_bij
plane_graph_image_e
plane_graph_image_i
plane_graph_image_iso
plane_graph_image_plane
plane_graph_image_v
plane_graph_mod
plane_planar
plus_e12
pointI_col
pointI_inj
pointI_inter
pointI_row
point_add
point_closure
point_dest_pt
point_inj
point_onto
point_scale
point_split
point_x
point_xy
polar_cont
polar_curve_lemma
polar_distinct
polar_euclid
polar_exist
polar_fg_inj
polar_inj
polar_nz
preimage
preimage_closed
preimage_compact
preimage_compact_interval
preimage_disjoint
preimage_first
preimage_restrict
preimage_subset
preimage_union
preimage_union2
preimage_unions
prod
prod_DEF
prod_EXISTS
proj_cauchy
proj_contraction
proj_d_euclid
proj_euclid1
psegment_cls
psegment_delete_end
psegment_edge
psegment_endpoint
psegment_order
psegment_order'
psegment_order_induct_lemma
psegment_subset_endpoint
psegment_triple2
psegment_triple3
psegment_triple_odd_even
pthm