HOL html

Files Index

Theorems Index

P (theorems)

PAIRWISE_DISJOINT_COMPONENTS
PAIRWISE_ORTHOGONAL_IMP_FINITE
PAIRWISE_ORTHOGONAL_INDEPENDENT
PARTIAL_DIVISION_EXTEND
PARTIAL_DIVISION_EXTEND_1
PARTIAL_DIVISION_EXTEND_INTERVAL
PARTIAL_DIVISION_OF_TAGGED_DIVISION
PARTIAL_SUMS_COMPONENT_LE_INFSUM
PARTIAL_SUMS_DROP_LE_INFSUM
PASTECART_ADD
PASTECART_AS_ORTHOGONAL_SUM
PASTECART_CMUL
PASTECART_EQ_VEC
PASTECART_IN_INTERIOR_SUBTOPOLOGY
PASTECART_NEG
PASTECART_SUB
PASTECART_VEC
PASTECART_VSUM
PASTING_LEMMA
PASTING_LEMMA_CLOSED
PASTING_LEMMA_EXISTS
PASTING_LEMMA_EXISTS_CLOSED
PATHFINISH_CIRCLEPATH
PATHFINISH_COMPOSE
PATHFINISH_IN_PATH_IMAGE
PATHFINISH_JOIN
PATHFINISH_LINEAR_IMAGE
PATHFINISH_LINEPATH
PATHFINISH_PARTCIRCLEPATH
PATHFINISH_REVERSEPATH
PATHFINISH_SHIFTPATH
PATHFINISH_SUBPATH
PATHFINISH_TRANSLATION
PATHINTEGRAL_CONVEX_PRIMITIVE
PATHSTART_CIRCLEPATH
PATHSTART_COMPOSE
PATHSTART_IN_PATH_IMAGE
PATHSTART_JOIN
PATHSTART_LINEAR_IMAGE_EQ
PATHSTART_LINEPATH
PATHSTART_PARTCIRCLEPATH
PATHSTART_REVERSEPATH
PATHSTART_SHIFTPATH
PATHSTART_SUBPATH
PATHSTART_TRANSLATION
PATH_APPROX_VECTOR_POLYNOMIAL_FUNCTION
PATH_ASSOC
PATH_COMPONENT
PATH_COMPONENT_DISJOINT
PATH_COMPONENT_EMPTY
PATH_COMPONENT_EQ
PATH_COMPONENT_EQ_CONNECTED_COMPONENT
PATH_COMPONENT_EQ_EMPTY
PATH_COMPONENT_EQ_EQ
PATH_COMPONENT_IMP_HOMOTOPIC_POINTS
PATH_COMPONENT_IN
PATH_COMPONENT_LINEAR_IMAGE
PATH_COMPONENT_MAXIMAL
PATH_COMPONENT_MONO
PATH_COMPONENT_OF_SUBSET
PATH_COMPONENT_PATH_COMPONENT
PATH_COMPONENT_PATH_IMAGE_PATHSTART
PATH_COMPONENT_REFL
PATH_COMPONENT_REFL_EQ
PATH_COMPONENT_SET
PATH_COMPONENT_SUBSET
PATH_COMPONENT_SUBSET_CONNECTED_COMPONENT
PATH_COMPONENT_SYM
PATH_COMPONENT_SYM_EQ
PATH_COMPONENT_TRANS
PATH_COMPONENT_TRANSLATION
PATH_COMPONENT_UNIV
PATH_COMPOSE_JOIN
PATH_COMPOSE_REVERSEPATH
PATH_CONNECTED_ANNULUS
PATH_CONNECTED_ARCWISE
PATH_CONNECTED_ARC_COMPLEMENT
PATH_CONNECTED_COMPLEMENT_ABSOLUTE_RETRACT
PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX
PATH_CONNECTED_COMPLEMENT_CARD_LT
PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_CONVEX_COMPACT
PATH_CONNECTED_COMPONENT_SET
PATH_CONNECTED_CONTINUOUS_IMAGE
PATH_CONNECTED_CONVEX_DIFF_CARD_LT
PATH_CONNECTED_DIFF_BALL
PATH_CONNECTED_EMPTY
PATH_CONNECTED_EQ_CONNECTED
PATH_CONNECTED_EQ_CONNECTED_LPC
PATH_CONNECTED_EQ_HOMOTOPIC_POINTS
PATH_CONNECTED_IFF_PATH_COMPONENT
PATH_CONNECTED_IMP_CONNECTED
PATH_CONNECTED_INTERVAL
PATH_CONNECTED_LINEAR_IMAGE
PATH_CONNECTED_LINEAR_IMAGE_EQ
PATH_CONNECTED_LINEPATH
PATH_CONNECTED_NEGATIONS
PATH_CONNECTED_OPEN_DELETE
PATH_CONNECTED_OPEN_DIFF_CARD_LT
PATH_CONNECTED_OPEN_DIFF_COUNTABLE
PATH_CONNECTED_OPEN_IN_DIFF_CARD_LT
PATH_CONNECTED_PATH_COMPONENT
PATH_CONNECTED_PATH_IMAGE
PATH_CONNECTED_PCROSS
PATH_CONNECTED_PCROSS_EQ
PATH_CONNECTED_PUNCTURED_BALL
PATH_CONNECTED_PUNCTURED_UNIVERSE
PATH_CONNECTED_SCALING
PATH_CONNECTED_SEGMENT
PATH_CONNECTED_SEMIOPEN_SEGMENT
PATH_CONNECTED_SING
PATH_CONNECTED_SPHERE
PATH_CONNECTED_SPHERE_EQ
PATH_CONNECTED_SUMS
PATH_CONNECTED_TRANSLATION
PATH_CONNECTED_TRANSLATION_EQ
PATH_CONNECTED_UNION
PATH_CONNECTED_UNIV
PATH_CONTAINS_ARC
PATH_CONTINUOUS_IMAGE
PATH_EQ
PATH_IMAGE_CIRCLEPATH
PATH_IMAGE_COMPOSE
PATH_IMAGE_JOIN
PATH_IMAGE_JOIN_SUBSET
PATH_IMAGE_LINEAR_IMAGE
PATH_IMAGE_LINEPATH
PATH_IMAGE_NONEMPTY
PATH_IMAGE_PARTCIRCLEPATH
PATH_IMAGE_PARTCIRCLEPATH_SUBSET
PATH_IMAGE_REVERSEPATH
PATH_IMAGE_SHIFTPATH
PATH_IMAGE_SUBPATH
PATH_IMAGE_SUBPATH_GEN
PATH_IMAGE_SUBPATH_SUBSET
PATH_IMAGE_SYM
PATH_IMAGE_TRANSLATION
PATH_INTEGRABLE_ADD
PATH_INTEGRABLE_COMPLEX_DIV
PATH_INTEGRABLE_COMPLEX_LMUL
PATH_INTEGRABLE_COMPLEX_RMUL
PATH_INTEGRABLE_CONTINUOUS_CIRCLEPATH
PATH_INTEGRABLE_CONTINUOUS_LINEPATH
PATH_INTEGRABLE_CONTINUOUS_PARTCIRCLEPATH
PATH_INTEGRABLE_EQ
PATH_INTEGRABLE_HOLOMORPHIC
PATH_INTEGRABLE_HOLOMORPHIC_SIMPLE
PATH_INTEGRABLE_INVERSEDIFF
PATH_INTEGRABLE_JOIN
PATH_INTEGRABLE_NEG
PATH_INTEGRABLE_ON
PATH_INTEGRABLE_REVERSEPATH
PATH_INTEGRABLE_REVERSEPATH_EQ
PATH_INTEGRABLE_SUB
PATH_INTEGRABLE_SUBPATH
PATH_INTEGRABLE_SUBPATH_REFL
PATH_INTEGRABLE_VSUM
PATH_INTEGRAL_0
PATH_INTEGRAL_ADD
PATH_INTEGRAL_BOUND_EXISTS
PATH_INTEGRAL_BOUND_LINEPATH
PATH_INTEGRAL_COMPLEX_DIV
PATH_INTEGRAL_COMPLEX_LMUL
PATH_INTEGRAL_COMPLEX_RMUL
PATH_INTEGRAL_CONST_LINEPATH
PATH_INTEGRAL_EQ
PATH_INTEGRAL_EQ_0
PATH_INTEGRAL_INTEGRAL
PATH_INTEGRAL_JOIN
PATH_INTEGRAL_LOCAL_PRIMITIVE
PATH_INTEGRAL_LOCAL_PRIMITIVE_ANY
PATH_INTEGRAL_LOCAL_PRIMITIVE_LEMMA
PATH_INTEGRAL_MIDPOINT
PATH_INTEGRAL_NEG
PATH_INTEGRAL_PRIMITIVE
PATH_INTEGRAL_PRIMITIVE_LEMMA
PATH_INTEGRAL_REVERSEPATH
PATH_INTEGRAL_REVERSE_LINEPATH
PATH_INTEGRAL_SHIFTPATH
PATH_INTEGRAL_SPLIT
PATH_INTEGRAL_SPLIT_LINEPATH
PATH_INTEGRAL_SUB
PATH_INTEGRAL_SUBPATH_COMBINE
PATH_INTEGRAL_SUBPATH_INTEGRAL
PATH_INTEGRAL_SUBPATH_REFL
PATH_INTEGRAL_SWAP
PATH_INTEGRAL_TRIVIAL
PATH_INTEGRAL_UNIFORM_LIMIT
PATH_INTEGRAL_UNIFORM_LIMIT_CIRCLEPATH
PATH_INTEGRAL_UNIQUE
PATH_INTEGRAL_VSUM
PATH_JOIN
PATH_JOIN_EQ
PATH_JOIN_IMP
PATH_JOIN_PATH_ENDS
PATH_LENGTH_DIFFERENTIABLE
PATH_LENGTH_JOIN
PATH_LENGTH_REVERSEPATH
PATH_LENGTH_VALID_PATH
PATH_LINEAR_IMAGE_EQ
PATH_LINEPATH
PATH_PARTCIRCLEPATH
PATH_REVERSEPATH
PATH_SHIFTPATH
PATH_SUBPATH
PATH_SYM
PATH_TRANSLATION_EQ
PATH_VECTOR_POLYNOMIAL_FUNCTION
PCROSS_AS_ORTHOGONAL_SUM
PCROSS_INTERVAL
PI2_BOUNDS
PIECEWISE_DIFFERENTIABLE_ADD
PIECEWISE_DIFFERENTIABLE_AFFINE
PIECEWISE_DIFFERENTIABLE_CASES
PIECEWISE_DIFFERENTIABLE_COMPOSE
PIECEWISE_DIFFERENTIABLE_NEG
PIECEWISE_DIFFERENTIABLE_ON_IMP_CONTINUOUS_ON
PIECEWISE_DIFFERENTIABLE_ON_SUBSET
PIECEWISE_DIFFERENTIABLE_SUB
PI_APPROX_32
PI_NZ
PI_POS
PI_POS_LE
PI_WORKS
PLANE_AFFINE_HULL_3
PLANE_LINEAR_IMAGE
PLANE_LINEAR_IMAGE_EQ
PLANE_TRANSLATION
PLANE_TRANSLATION_EQ
POINTS_IN_CONVEX_HULL
POINTWISE_ANTISYM
POLE_LEMMA
POLE_LEMMA_OPEN
POLE_THEOREM
POLE_THEOREM_0
POLE_THEOREM_ANALYTIC
POLE_THEOREM_ANALYTIC_0
POLE_THEOREM_ANALYTIC_OPEN_SUPERSET
POLE_THEOREM_ANALYTIC_OPEN_SUPERSET_0
POLE_THEOREM_OPEN
POLE_THEOREM_OPEN_0
POLYHEDRON_AFFINE_HULL
POLYHEDRON_AFF_GE
POLYHEDRON_AS_CONE_PLUS_CONV
POLYHEDRON_COLLINEAR_FACES
POLYHEDRON_COLLINEAR_FACES_STRONG
POLYHEDRON_CONVEX_CONE_HULL
POLYHEDRON_CONVEX_HULL
POLYHEDRON_EMPTY
POLYHEDRON_EQ_FINITE_EXPOSED_FACES
POLYHEDRON_EQ_FINITE_FACES
POLYHEDRON_HALFSPACE_GE
POLYHEDRON_HALFSPACE_LE
POLYHEDRON_HYPERPLANE
POLYHEDRON_IMP_CLOSED
POLYHEDRON_IMP_CONVEX
POLYHEDRON_INTER
POLYHEDRON_INTERS
POLYHEDRON_INTERVAL
POLYHEDRON_INTER_AFFINE
POLYHEDRON_INTER_AFFINE_MINIMAL
POLYHEDRON_INTER_AFFINE_PARALLEL
POLYHEDRON_INTER_AFFINE_PARALLEL_MINIMAL
POLYHEDRON_INTER_POLYTOPE
POLYHEDRON_LINEAR_IMAGE
POLYHEDRON_LINEAR_IMAGE_EQ
POLYHEDRON_NEGATIONS
POLYHEDRON_POLYTOPE_SUMS
POLYHEDRON_POSITIVE_ORTHANT
POLYHEDRON_RIDGE_TWO_FACETS
POLYHEDRON_SUMS
POLYHEDRON_TRANSLATION_EQ
POLYHEDRON_UNIV
POLYTOPE_CONVEX_HULL
POLYTOPE_EMPTY
POLYTOPE_EQ_BOUNDED_POLYHEDRON
POLYTOPE_FACET_EXISTS
POLYTOPE_FACET_LOWER_BOUND
POLYTOPE_IMP_BOUNDED
POLYTOPE_IMP_CLOSED
POLYTOPE_IMP_COMPACT
POLYTOPE_IMP_CONVEX
POLYTOPE_IMP_POLYHEDRON
POLYTOPE_INTER
POLYTOPE_INTERVAL
POLYTOPE_INTER_POLYHEDRON
POLYTOPE_LINEAR_IMAGE
POLYTOPE_LINEAR_IMAGE_EQ
POLYTOPE_NEGATIONS
POLYTOPE_PCROSS
POLYTOPE_PCROSS_EQ
POLYTOPE_SCALING
POLYTOPE_SCALING_EQ
POLYTOPE_SING
POLYTOPE_SUMS
POLYTOPE_TRANSLATION_EQ
POLYTOPE_UNION_CONVEX_HULL_FACETS
POLYTOPE_VERTEX_LOWER_BOUND
POWER_REAL_SERIES_CONV_IMP_ABSCONV_WEAK
POWER_SERIES_ANALYTIC
POWER_SERIES_AND_DERIVATIVE
POWER_SERIES_AND_DERIVATIVE_0
POWER_SERIES_CONV_IMP_ABSCONV
POWER_SERIES_CONV_IMP_ABSCONV_WEAK
POWER_SERIES_HOLOMORPHIC
POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ
POWER_SERIES_UNIFORM_CONVERGENCE_STOLZ_1
POW_2_CSQRT
POW_2_SQRT
POW_2_SQRT_ABS
PRESERVES_LEBESGUE_MEASURABLE_IMP_PRESERVES_NEGLIGIBLE
PRESERVES_NORM_INJECTIVE
PRESERVES_NORM_PRESERVES_DOT
PRODUCT_1
PRODUCT_2
PRODUCT_3
PRODUCT_4
PRODUCT_ASSOCIATIVE
PRODUCT_MBASIS
PRODUCT_MBASIS_SING
PRODUCT_PERMUTE
PRODUCT_PERMUTE_NUMSEG
PROPERTY_EMPTY_INTERVAL
PROPER_MAP
PROPER_MAP_FROM_COMPACT
PUSHIN_DROPOUT
PYTHAGORAS
P_HULL
Product_DEF
pad2d3d
partcirclepath
path
path_component
path_connected
path_image
path_integrable_on
path_integral
path_length
pathfinish
pathstart
pi
piecewise_differentiable_on
plane
polyhedron
polytope
primitive
pth
pth_zero
pushin