HOL html

Files Index

Theorems Index

S (theorems)

SAME_DISTANCES_TO_AFFINE_HULL
SCALING_LINEAR
SCHAUDER
SCHAUDER_PROJECTION
SCHAUDER_UNIV
SCHOTTKY
SCHWARZ_LEMMA
SCHWARZ_REFLECTION
SDIFF
SECOND_CARTAN_THM_DIM_1
SECOND_MEAN_VALUE_THEOREM
SECOND_MEAN_VALUE_THEOREM_BONNET
SECOND_MEAN_VALUE_THEOREM_BONNET_FULL
SECOND_MEAN_VALUE_THEOREM_FULL
SECOND_MEAN_VALUE_THEOREM_GEN
SECOND_MEAN_VALUE_THEOREM_GEN_FULL
SEGMENTS_SUBSET_CONVEX_HULL
SEGMENT_1
SEGMENT_AS_BALL
SEGMENT_BOUND
SEGMENT_CLOSED_OPEN
SEGMENT_CONVEX_HULL
SEGMENT_EDGE_OF
SEGMENT_EQ
SEGMENT_EQ_EMPTY
SEGMENT_EQ_SING
SEGMENT_FACE_OF
SEGMENT_FURTHEST_LE
SEGMENT_HORIZONTAL
SEGMENT_IMAGE_INTERVAL
SEGMENT_OPEN_SUBSET_CLOSED
SEGMENT_REAL_SEGMENT
SEGMENT_REFL
SEGMENT_SCALAR_MULTIPLE
SEGMENT_SUBSET_HALFLINE
SEGMENT_SYM
SEGMENT_TO_CLOSEST_POINT
SEGMENT_TO_POINT_EXISTS
SEGMENT_TRANSLATION
SEGMENT_VERTICAL
SELF_ADJOINT_COMPOSE
SELF_ADJOINT_HAS_EIGENVECTOR
SELF_ADJOINT_HAS_EIGENVECTOR_BASIS
SELF_ADJOINT_HAS_EIGENVECTOR_BASIS_OF_SUBSPACE
SELF_ADJOINT_HAS_EIGENVECTOR_IN_SUBSPACE
SELF_ADJOINT_ORTHOGONAL_EIGENVECTORS
SEPARABLE
SEPARATE_CLOSED_COMPACT
SEPARATE_CLOSED_CONES
SEPARATE_COMPACT_CLOSED
SEPARATE_POINT_CLOSED
SEPARATING_HYPERPLANE_CLOSED_0
SEPARATING_HYPERPLANE_CLOSED_0_INSET
SEPARATING_HYPERPLANE_CLOSED_COMPACT
SEPARATING_HYPERPLANE_CLOSED_POINT
SEPARATING_HYPERPLANE_CLOSED_POINT_INSET
SEPARATING_HYPERPLANE_COMPACT_CLOSED
SEPARATING_HYPERPLANE_COMPACT_CLOSED_NONZERO
SEPARATING_HYPERPLANE_COMPACT_COMPACT
SEPARATING_HYPERPLANE_POLYHEDRA
SEPARATING_HYPERPLANE_RELATIVE_INTERIORS
SEPARATING_HYPERPLANE_SETS
SEPARATING_HYPERPLANE_SET_0
SEPARATING_HYPERPLANE_SET_0_INSPAN
SEPARATING_HYPERPLANE_SET_POINT_INAFF
SEPARATION_CLOSURES
SEPARATION_HAUSDORFF
SEPARATION_NORMAL
SEPARATION_NORMAL_COMPACT
SEPARATION_T0
SEPARATION_T1
SEPARATION_T2
SEQITERATE_CLAUSES
SEQITERATE_ITERATE
SEQUENCE_CAUCHY_WLOG
SEQUENCE_INFINITE_LEMMA
SEQUENCE_UNIQUE_LIMPT
SEQUENTIALLY
SEQ_HARMONIC
SEQ_MONO_LEMMA
SEQ_OFFSET
SEQ_OFFSET_NEG
SEQ_OFFSET_REV
SERIES_0
SERIES_ABSCONV_IMP_CONV
SERIES_ADD
SERIES_AND_DERIVATIVE_COMPARISON
SERIES_AND_DERIVATIVE_COMPARISON_COMPLEX
SERIES_AND_DERIVATIVE_COMPARISON_LOCAL
SERIES_CAUCHY
SERIES_CAUCHY_UNIFORM
SERIES_CMUL
SERIES_COMPARISON
SERIES_COMPARISON_COMPLEX
SERIES_COMPARISON_UNIFORM
SERIES_COMPARISON_UNIFORM_COMPLEX
SERIES_COMPLEX_DIV
SERIES_COMPLEX_LMUL
SERIES_COMPLEX_RMUL
SERIES_COMPONENT
SERIES_DIFFERENTIABLE_COMPARISON_COMPLEX
SERIES_DIFFS
SERIES_DIRICHLET
SERIES_DIRICHLET_BILINEAR
SERIES_DIRICHLET_COMPLEX
SERIES_DIRICHLET_COMPLEX_EXPLICIT
SERIES_DIRICHLET_COMPLEX_GEN
SERIES_DIRICHLET_COMPLEX_VERY_EXPLICIT
SERIES_FINITE
SERIES_FINITE_SUPPORT
SERIES_FROM
SERIES_GOESTOZERO
SERIES_INJECTIVE_IMAGE
SERIES_INJECTIVE_IMAGE_STRONG
SERIES_LIFT_ABSCONV_IMP_CONV
SERIES_LINEAR
SERIES_NEG
SERIES_RATIO
SERIES_REARRANGE
SERIES_REARRANGE_EQ
SERIES_RESTRICT
SERIES_SUB
SERIES_SUBSET
SERIES_TRIVIAL
SERIES_UNIQUE
SERIES_VSUM
SETCODE_BOUNDS
SETDIST_CLOSED_COMPACT
SETDIST_CLOSEST_POINT
SETDIST_CLOSURE
SETDIST_COMPACT_CLOSED
SETDIST_DIFFERENCES
SETDIST_EMPTY
SETDIST_EQ_0_BOUNDED
SETDIST_EQ_0_CLOSED_COMPACT
SETDIST_EQ_0_COMPACT_CLOSED
SETDIST_EQ_0_SING
SETDIST_LE_DIST
SETDIST_LINEAR_IMAGE
SETDIST_LIPSCHITZ
SETDIST_POS_LE
SETDIST_REFL
SETDIST_SINGS
SETDIST_SUBSET_LEFT
SETDIST_SUBSET_RIGHT
SETDIST_SYM
SETDIST_TRANSLATION
SETDIST_TRIANGLE
SETDIST_UNIQUE
SETVARIATION_EQUAL_LEMMA
SET_VARIATION
SET_VARIATION_0
SET_VARIATION_ELEMENTARY_LEMMA
SET_VARIATION_EQ
SET_VARIATION_GE_FUNCTION
SET_VARIATION_LBOUND
SET_VARIATION_LBOUND_ON_INTERVAL
SET_VARIATION_MONOTONE
SET_VARIATION_ON_DIVISION
SET_VARIATION_ON_ELEMENTARY
SET_VARIATION_ON_INTERVAL
SET_VARIATION_ON_NULL
SET_VARIATION_POS_LE
SET_VARIATION_TRIANGLE
SET_VARIATION_UBOUND
SET_VARIATION_UBOUND_ON_INTERVAL
SET_VARIATION_WORKS_ON_INTERVAL
SHIFTPATH_LINEAR_IMAGE
SHIFTPATH_SHIFTPATH
SHIFTPATH_TRANSLATION
SHIFTPATH_TRIVIAL
SIGMA_COMPACT
SIMPLEX
SIMPLEX_DIM_GE
SIMPLEX_EMPTY
SIMPLEX_EXPLICIT
SIMPLEX_EXTREMAL_LE
SIMPLEX_EXTREMAL_LE_EXISTS
SIMPLEX_EXTREME_POINTS
SIMPLEX_FACE_OF_SIMPLEX
SIMPLEX_FURTHEST_LE
SIMPLEX_FURTHEST_LE_EXISTS
SIMPLEX_FURTHEST_LT
SIMPLEX_IMP_POLYTOPE
SIMPLEX_MINUS_1
SIMPLEX_TOP_FACE
SIMPLE_CLOSED_PATH_ABS_WINDING_NUMBER_INSIDE
SIMPLE_CLOSED_PATH_NORM_WINDING_NUMBER_INSIDE
SIMPLE_CLOSED_PATH_WINDING_NUMBER_CASES
SIMPLE_CLOSED_PATH_WINDING_NUMBER_INSIDE
SIMPLE_CLOSED_PATH_WINDING_NUMBER_POS
SIMPLE_PATH_ASSOC
SIMPLE_PATH_CASES
SIMPLE_PATH_CIRCLEPATH
SIMPLE_PATH_ENDLESS
SIMPLE_PATH_EQ_ARC
SIMPLE_PATH_IMP_ARC
SIMPLE_PATH_IMP_PATH
SIMPLE_PATH_JOIN_IMP
SIMPLE_PATH_JOIN_LOOP
SIMPLE_PATH_JOIN_LOOP_EQ
SIMPLE_PATH_LINEAR_IMAGE_EQ
SIMPLE_PATH_LINEPATH
SIMPLE_PATH_LINEPATH_EQ
SIMPLE_PATH_PARTCIRCLEPATH
SIMPLE_PATH_REVERSEPATH
SIMPLE_PATH_SHIFTPATH
SIMPLE_PATH_SUBPATH
SIMPLE_PATH_SUBPATH_EQ
SIMPLE_PATH_SYM
SIMPLE_PATH_TRANSLATION_EQ
SIMPLICIAL_COMPLEX_IMP_TRIANGULATION
SIMPLY_CONNECTED_EMPTY
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_LOOP_ALL
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_LOOP_ANY
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_LOOP_SOME
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_PATH
SIMPLY_CONNECTED_EQ_HOMOTOPIC_PATHS
SIMPLY_CONNECTED_IMP_CONNECTED
SIMPLY_CONNECTED_IMP_PATH_CONNECTED
SIMPLY_CONNECTED_IMP_WINDING_NUMBER_ZERO
SIMPLY_CONNECTED_INJECTIVE_LINEAR_IMAGE
SIMPLY_CONNECTED_INSIDE_SIMPLE_PATH
SIMPLY_CONNECTED_INTER
SIMPLY_CONNECTED_PCROSS
SIMPLY_CONNECTED_PCROSS_EQ
SIMPLY_CONNECTED_RETRACTION_GEN
SIMPLY_CONNECTED_SPHERE
SIMPLY_CONNECTED_SPHERE_EQ
SIMPLY_CONNECTED_TRANSLATION
SIMPLY_CONNECTED_UNION
SINCOS_PRINCIPAL_VALUE
SINCOS_TOTAL_2PI
SINCOS_TOTAL_PI
SINCOS_TOTAL_PI2
SIN_0
SIN_ACS
SIN_ACS_NZ
SIN_ADD
SIN_ANGLE
SIN_ANGLE_EQ
SIN_ANGLE_EQ_0
SIN_ANGLE_POS
SIN_ASN
SIN_ATN
SIN_BOUNDS
SIN_CIRCLE
SIN_COS
SIN_COS_EQ
SIN_COS_INJ
SIN_COS_SQRT
SIN_DOUBLE
SIN_EQ
SIN_EQ_0
SIN_EQ_0_PI
SIN_EQ_1
SIN_EQ_MINUS1
SIN_HASZERO
SIN_HASZERO_MINIMAL
SIN_INJ_PI
SIN_INTEGER_2PI
SIN_INTEGER_PI
SIN_MONO_LE
SIN_MONO_LE_EQ
SIN_MONO_LT
SIN_MONO_LT_EQ
SIN_NEARZERO
SIN_NEG
SIN_NONTRIVIAL
SIN_NPI
SIN_PERIODIC
SIN_PERIODIC_PI
SIN_PI
SIN_PI2
SIN_PI6
SIN_PI6_STRADDLE
SIN_PIMUL_EQ_0
SIN_POS_PI
SIN_POS_PI2
SIN_POS_PI_LE
SIN_POS_PI_REV
SIN_SQUARED_ANGLE
SIN_SQUARED_VECTOR_ANGLE
SIN_SUB
SIN_TAN
SIN_TOTAL_POS
SIN_VECTOR_ANGLE
SIN_VECTOR_ANGLE_EQ
SIN_VECTOR_ANGLE_EQ_0
SIN_VECTOR_ANGLE_POS
SIN_ZERO
SIN_ZERO_PI
SLICE_123
SLICE_312
SLICE_BALL
SLICE_CBALL
SLICE_DIFF
SLICE_DROPOUT_3
SLICE_EMPTY
SLICE_INTER
SLICE_INTERVAL
SLICE_SPECIAL_WEDGE
SLICE_SUBSET
SLICE_UNION
SLICE_UNIONS
SLICE_UNIV
SNDCART_ADD
SNDCART_CMUL
SNDCART_NEG
SNDCART_SUB
SNDCART_VEC
SNDCART_VSUM
SOLID_TRIANGLE_CONGRUENT_NEG
SPANNING_SUBSET_INDEPENDENT
SPANNING_SURJECTIVE_IMAGE
SPANS_IMAGE
SPAN_0
SPAN_2
SPAN_3
SPAN_ADD
SPAN_ADD_EQ
SPAN_BREAKDOWN
SPAN_BREAKDOWN_EQ
SPAN_CARD_GE_DIM
SPAN_CLAUSES
SPAN_CONVEX_CONE_ALLSIGNS
SPAN_DELETE_0
SPAN_EMPTY
SPAN_EQ
SPAN_EQ_DIM
SPAN_EQ_INSERT
SPAN_EQ_SELF
SPAN_EXPLICIT
SPAN_FINITE
SPAN_IMAGE_SCALE
SPAN_INC
SPAN_INDUCT
SPAN_INDUCT_ALT
SPAN_INSERT_0
SPAN_LINEAR_IMAGE
SPAN_MBASIS
SPAN_MONO
SPAN_MUL
SPAN_MUL_EQ
SPAN_NEG
SPAN_NEG_EQ
SPAN_NOT_UNIV_ORTHOGONAL
SPAN_NOT_UNIV_SUBSET_HYPERPLANE
SPAN_OF_SUBSPACE
SPAN_OPEN
SPAN_PCROSS
SPAN_PCROSS_SUBSET
SPAN_SING
SPAN_SPAN
SPAN_STDBASIS
SPAN_SUB
SPAN_SUBSET_SUBSPACE
SPAN_SUBSPACE
SPAN_SUMS
SPAN_SUPERSET
SPAN_TRANS
SPAN_UNION
SPAN_UNION_SUBSET
SPAN_UNIV
SPAN_VSUM
SPECIAL_HYPERPLANE_SPAN
SPHERE_1
SPHERE_EMPTY
SPHERE_EQ_EMPTY
SPHERE_EQ_SING
SPHERE_LINEAR_IMAGE
SPHERE_RETRACT_OF_PUNCTURED_UNIVERSE
SPHERE_RETRACT_OF_PUNCTURED_UNIVERSE_GEN
SPHERE_SING
SPHERE_SUBSET_CBALL
SPHERE_TRANSLATION
SPHERE_UNION_BALL
SPHERICAL_COORDINATES
SPLIT_INSIDE_SIMPLE_CLOSED_CURVE
SQNORM_PASTECART
SQRT_0
SQRT_1
SQRT_DIV
SQRT_EQ_0
SQRT_EVEN_POW2
SQRT_INJ
SQRT_INV
SQRT_LT_0
SQRT_MONO_LE
SQRT_MONO_LE_EQ
SQRT_MONO_LT
SQRT_MONO_LT_EQ
SQRT_MUL
SQRT_POS_LE
SQRT_POS_LT
SQRT_POW2
SQRT_POW_2
SQRT_UNIQUE
SQRT_WORKS
SQUARE_BOUND_LEMMA
SQUARE_CONTINUOUS
STARLIKE_CLOSURE
STARLIKE_COMPACT_PROJECTIVE
STARLIKE_CONVEX_SUBSET
STARLIKE_CONVEX_TWEAK_BOUNDARY_POINTS
STARLIKE_IMP_CONNECTED
STARLIKE_IMP_CONTRACTIBLE
STARLIKE_IMP_CONTRACTIBLE_GEN
STARLIKE_IMP_PATH_CONNECTED
STARLIKE_IMP_SIMPLY_CONNECTED
STARLIKE_LINEAR_IMAGE
STARLIKE_LINEAR_IMAGE_EQ
STARLIKE_NEGLIGIBLE
STARLIKE_NEGLIGIBLE_BOUNDED_MEASURABLE
STARLIKE_NEGLIGIBLE_LEMMA
STARLIKE_NEGLIGIBLE_STRONG
STARLIKE_PCROSS
STARLIKE_PCROSS_EQ
STARLIKE_TRANSLATION_EQ
STARLIKE_UNIV
STD_SIMPLEX
STEINHAUS
STEINHAUS_LEBESGUE
STEINHAUS_TRIVIAL
STONE_WEIERSTRASS
STONE_WEIERSTRASS_ALT
STONE_WEIERSTRASS_REAL_POLYNOMIAL_FUNCTION
STONE_WEIERSTRASS_VECTOR_POLYNOMIAL_FUNCTION
STONE_WEIERSTRASS_VECTOR_POLYNOMIAL_FUNCTION_AFFINE
STONE_WEIERSTRASS_VECTOR_POLYNOMIAL_FUNCTION_SUBSPACE
STRETCH_GALOIS
SUBADDITIVE_CONTENT_DIVISION
SUBPATH_LINEAR_IMAGE
SUBPATH_REFL
SUBPATH_REVERSEPATH
SUBPATH_SCALING_LEMMA
SUBPATH_TO_FRONTIER
SUBPATH_TO_FRONTIER_EXPLICIT
SUBPATH_TO_FRONTIER_STRONG
SUBPATH_TRANSLATION
SUBPATH_TRIVIAL
SUBSEQUENCE_DIAGONALIZATION_LEMMA
SUBSET_AFFINE_HULL_SPECIAL_SCALE
SUBSET_BALL
SUBSET_BALLS
SUBSET_CBALL
SUBSET_CLOSURE
SUBSET_CONTINUOUS_IMAGE_SEGMENT_1
SUBSET_DROP_IMAGE
SUBSET_FACE_OF_SIMPLEX
SUBSET_HULL
SUBSET_HYPERPLANES
SUBSET_INTERIOR
SUBSET_INTERVAL
SUBSET_INTERVAL_1
SUBSET_INTERVAL_IMP
SUBSET_LE_DIM
SUBSET_LIFT_IMAGE
SUBSET_OF_FACE_OF
SUBSET_PATH_IMAGE_JOIN
SUBSET_REAL_INTERVAL
SUBSET_RELATIVE_INTERIOR
SUBSET_SECOND_COUNTABLE
SUBSET_SEGMENT
SUBSET_SEGMENT_OPEN_CLOSED
SUBSPACE_0
SUBSPACE_ADD
SUBSPACE_BOUNDED_EQ_TRIVIAL
SUBSPACE_CONVEX_CONE_SYMMETRIC
SUBSPACE_HYPERPLANE
SUBSPACE_IMP_AFFINE
SUBSPACE_IMP_CONIC
SUBSPACE_IMP_CONVEX
SUBSPACE_IMP_CONVEX_CONE
SUBSPACE_IMP_NONEMPTY
SUBSPACE_INTER
SUBSPACE_INTERS
SUBSPACE_ISOMORPHISM
SUBSPACE_KERNEL
SUBSPACE_LINEAR_FIXED_POINTS
SUBSPACE_LINEAR_IMAGE
SUBSPACE_LINEAR_IMAGE_EQ
SUBSPACE_LINEAR_PREIMAGE
SUBSPACE_MUL
SUBSPACE_NEG
SUBSPACE_ORTHOGONAL_TO_VECTOR
SUBSPACE_ORTHOGONAL_TO_VECTORS
SUBSPACE_PCROSS
SUBSPACE_PCROSS_EQ
SUBSPACE_SPAN
SUBSPACE_SPECIAL_HYPERPLANE
SUBSPACE_SUB
SUBSPACE_SUBSTANDARD
SUBSPACE_SUMS
SUBSPACE_TRANSLATION_SELF
SUBSPACE_TRANSLATION_SELF_EQ
SUBSPACE_TRIVIAL
SUBSPACE_UNION_CHAIN
SUBSPACE_UNIV
SUBSPACE_VSUM
SUBTOPOLOGY_SUPERSET
SUBTOPOLOGY_TOPSPACE
SUBTOPOLOGY_UNIV
SUMMABLE_0
SUMMABLE_ADD
SUMMABLE_BILINEAR_PARTIAL_PRE
SUMMABLE_CAUCHY
SUMMABLE_CMUL
SUMMABLE_COMPARISON
SUMMABLE_COMPLEX_DIV
SUMMABLE_COMPLEX_LMUL
SUMMABLE_COMPLEX_RMUL
SUMMABLE_COMPONENT
SUMMABLE_EQ
SUMMABLE_EQ_COFINITE
SUMMABLE_EQ_EVENTUALLY
SUMMABLE_FROM_ELSEWHERE
SUMMABLE_GP
SUMMABLE_IFF
SUMMABLE_IFF_COFINITE
SUMMABLE_IFF_EVENTUALLY
SUMMABLE_IMP_BOUNDED
SUMMABLE_IMP_SUMS_BOUNDED
SUMMABLE_IMP_TOZERO
SUMMABLE_LINEAR
SUMMABLE_NEG
SUMMABLE_REARRANGE
SUMMABLE_REINDEX
SUMMABLE_RESTRICT
SUMMABLE_SUB
SUMMABLE_SUBSET
SUMMABLE_SUBSET_ABSCONV
SUMMABLE_SUBSET_COMPLEX
SUMMABLE_TRIVIAL
SUMS_0
SUMS_CNJ
SUMS_COMPLEX_0
SUMS_EQ
SUMS_FINITE_DIFF
SUMS_FINITE_UNION
SUMS_GP
SUMS_IFF
SUMS_INFSUM
SUMS_INTERVALS
SUMS_LIM
SUMS_OFFSET
SUMS_OFFSET_REV
SUMS_REINDEX
SUMS_SUMMABLE
SUM_1
SUM_2
SUM_3
SUM_4
SUM_BERNSTEIN
SUM_CONTENT_AREA_OVER_THIN_DIVISION
SUM_GP
SUM_GP_BASIC
SUM_GP_MULTIPLIED
SUM_GP_OFFSET
SUM_INTEGRAL_BOUNDS_DECREASING
SUM_INTEGRAL_BOUNDS_INCREASING
SUM_INTEGRAL_LBOUND_DECREASING
SUM_INTEGRAL_LBOUND_INCREASING
SUM_INTEGRAL_UBOUND_DECREASING
SUM_INTEGRAL_UBOUND_INCREASING
SUM_OVER_TAGGED_DIVISION_LEMMA
SUM_OVER_TAGGED_PARTIAL_DIVISION_LEMMA
SUM_VSUM
SUPPORTING_HYPERPLANE_CLOSED_POINT
SUPPORTING_HYPERPLANE_COMPACT_POINT_INF
SUPPORTING_HYPERPLANE_COMPACT_POINT_SUP
SUPPORTING_HYPERPLANE_RELATIVE_BOUNDARY
SUPPORTING_HYPERPLANE_RELATIVE_FRONTIER
SUP_INSERT
SURA_BURA_CLOSED
SURA_BURA_COMPACT
SURJECTIVE_SCALING
SUSSMANN_OPEN_MAPPING
SYLVESTER_DETERMINANT_IDENTITY
SYMDIFF_PARITY_LEMMA
SYMMETRIC_CLOSURE
SYMMETRIC_INTERIOR
SYMMETRIC_LINEAR_IMAGE
SYMMETRIC_MATRIX
SYMMETRIC_MATRIX_DIAGONALIZABLE_EXPLICIT
SYMMETRIC_MATRIX_EQ_DIAGONALIZABLE
SYMMETRIC_MATRIX_IMP_DIAGONALIZABLE
SYMMETRIC_MATRIX_MUL
SYMMETRIC_MATRIX_ORTHOGONAL_EIGENVECTORS
SYMMETRIX_MATRIX_CONJUGATE
scale
segment
semma
seqiterate
seqiterate_EXISTS
sequentially
set_variation
setcode
setdist
sgn_ge
sgn_gt
sgn_le
sgn_lt
shiftpath
simple_path
simplex
simplicial_complex
simply_connected
sin
sindex
slemma
slice
solid_triangle
span
special
sphere
sqrt
starlike
subpath
subspace
subtopology
summable
sums