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 | _ |
N (theorems)
NEARBY_INVERTIBLE_MATRIXNEGATIONS_BALL
NEGATIONS_CBALL
NEGATIONS_SPHERE
NEGLIGIBLE
NEGLIGIBLE_AFFINE_HULL
NEGLIGIBLE_AFFINE_HULL_1
NEGLIGIBLE_AFFINE_HULL_2
NEGLIGIBLE_AFFINE_HULL_3
NEGLIGIBLE_ARG_EQ
NEGLIGIBLE_CIRCULAR_CONE
NEGLIGIBLE_CIRCULAR_CONE_0
NEGLIGIBLE_CIRCULAR_CONE_0_NONPARALLEL
NEGLIGIBLE_CONVEX_FRONTIER
NEGLIGIBLE_CONVEX_HULL
NEGLIGIBLE_CONVEX_HULL_1
NEGLIGIBLE_CONVEX_HULL_2
NEGLIGIBLE_CONVEX_HULL_3
NEGLIGIBLE_CONVEX_HULL_DIFF_CONV0
NEGLIGIBLE_COUNTABLE
NEGLIGIBLE_COUNTABLE_UNIONS
NEGLIGIBLE_COUNTABLE_UNIONS_GEN
NEGLIGIBLE_DELETE
NEGLIGIBLE_DIFF
NEGLIGIBLE_DIFFERENTIABLE_IMAGE_LOWDIM
NEGLIGIBLE_DIFFERENTIABLE_IMAGE_NEGLIGIBLE
NEGLIGIBLE_EMPTY
NEGLIGIBLE_EQ_MEASURE_0
NEGLIGIBLE_FINITE
NEGLIGIBLE_FRONTIER_INTERVAL
NEGLIGIBLE_HYPERPLANE
NEGLIGIBLE_IFF_LEBESGUE_MEASURABLE_SUBSETS
NEGLIGIBLE_IFF_MEASURABLE_SUBSETS
NEGLIGIBLE_IMAGE_BOUNDED_VARIATION_INTERVAL
NEGLIGIBLE_IMP_LEBESGUE_MEASURABLE
NEGLIGIBLE_IMP_MEASURABLE
NEGLIGIBLE_INSERT
NEGLIGIBLE_INTER
NEGLIGIBLE_INTERVAL
NEGLIGIBLE_LINEAR_IMAGE
NEGLIGIBLE_LINEAR_IMAGE_EQ
NEGLIGIBLE_LINEAR_SINGULAR_IMAGE
NEGLIGIBLE_LIPSCHITZ_IMAGE_UNIV
NEGLIGIBLE_LOCALLY_LIPSCHITZ_IMAGE
NEGLIGIBLE_LOWDIM
NEGLIGIBLE_ON_INTERVALS
NEGLIGIBLE_ON_UNIV
NEGLIGIBLE_OUTER
NEGLIGIBLE_OUTER_LE
NEGLIGIBLE_RCONE_EQ
NEGLIGIBLE_RECTIFIABLE_PATH_IMAGE
NEGLIGIBLE_SING
NEGLIGIBLE_SPHERE
NEGLIGIBLE_STANDARD_HYPERPLANE
NEGLIGIBLE_SUBSET
NEGLIGIBLE_SYMDIFF_EQ
NEGLIGIBLE_TRANSLATION
NEGLIGIBLE_TRANSLATION_EQ
NEGLIGIBLE_TRANSLATION_REV
NEGLIGIBLE_UNION
NEGLIGIBLE_UNIONS
NEGLIGIBLE_UNION_EQ
NEGLIGIBLE_VALID_PATH_IMAGE
NEIGHBOURHOOD_EXTENSION_INTO_ANR
NEIGHBOURHOOD_EXTENSION_INTO_ANR_LOCAL
NEIGHBOURHOOD_RETRACT_IMP_ANR
NEIGHBOURHOOD_RETRACT_IMP_ANR_UNIV
NET
NETLIMIT_AT
NETLIMIT_ATREAL
NETLIMIT_WITHIN
NETLIMIT_WITHINREAL
NETLIMIT_WITHIN_INTERIOR
NET_DILEMMA
NEUTRAL_AND
NEUTRAL_COMPLEX_MUL
NEUTRAL_LIFTED
NEUTRAL_OUTER
NEUTRAL_VECTOR_ADD
NONEMPTY_SIMPLE_PATH_ENDLESS
NONNEGATIVE_ABSOLUTELY_INTEGRABLE
NONNEGATIVE_ABSOLUTELY_REAL_INTEGRABLE
NONTRIVIAL_LIMIT_WITHIN
NON_EXTENSIBLE_BORSUK_MAP
NORMBALL_BALL
NORM_0
NORM_1
NORM_1_POS
NORM_ADD_PYTHAGOREAN
NORM_AND_CROSS_EQ_0
NORM_BASIS
NORM_BASIS_1
NORM_BOUND_COMPONENT_LE
NORM_BOUND_COMPONENT_LT
NORM_BOUND_GENERALIZE
NORM_CAUCHY_SCHWARZ
NORM_CAUCHY_SCHWARZ_ABS
NORM_CAUCHY_SCHWARZ_ABS_EQ
NORM_CAUCHY_SCHWARZ_DIV
NORM_CAUCHY_SCHWARZ_EQ
NORM_CAUCHY_SCHWARZ_EQUAL
NORM_CCOS_LE
NORM_CCOS_PLUS1_LE
NORM_CCOS_POW_2
NORM_CEXP
NORM_CEXP_II
NORM_CEXP_IMAGINARY
NORM_COSSIN
NORM_CPOW_REAL
NORM_CPOW_REAL_MONO
NORM_CPRODUCT
NORM_CROSS
NORM_CROSS_DOT
NORM_CROSS_MULTIPLY
NORM_CSIN_POW_2
NORM_EQ
NORM_EQ_0
NORM_EQ_0_DOT
NORM_EQ_0_IMP
NORM_EQ_1
NORM_EQ_SQUARE
NORM_FSTCART
NORM_GE_SQUARE
NORM_GT_SQUARE
NORM_INCREASES_ONLINE
NORM_LE
NORM_LE_0
NORM_LE_COMPONENTWISE
NORM_LE_INFNORM
NORM_LE_L1
NORM_LE_PASTECART
NORM_LE_SQUARE
NORM_LIFT
NORM_LT
NORM_LT_SQUARE
NORM_LT_SQUARE_ALT
NORM_MUL
NORM_NEG
NORM_PAD2D3D
NORM_PASTECART
NORM_PASTECART_0
NORM_PASTECART_LE
NORM_POS_LE
NORM_POS_LT
NORM_POW_2
NORM_REAL
NORM_ROTATE2D
NORM_SCALING
NORM_SEGMENT_LOWERBOUND
NORM_SEGMENT_ORTHOGONAL_LOWERBOUND
NORM_SNDCART
NORM_SUB
NORM_SUM_LEMMA
NORM_TRIANGLE
NORM_TRIANGLE_EQ
NORM_TRIANGLE_LE
NORM_TRIANGLE_LT
NORM_TRIANGLE_SUB
NORM_VSUM_PYTHAGOREAN
NORM_VSUM_TRIVIAL_LEMMA
NOT_ABSOLUTE_RETRACT_COBOUNDED
NOT_BOUNDED_UNIV
NOT_COPLANAR_0_4_IMP_INDEPENDENT
NOT_COPLANAR_IMP_NOT_COLLINEAR_DROPOUT_3
NOT_COPLANAR_NOT_COLLINEAR
NOT_EVENTUALLY
NOT_INTERVAL_UNIV
NOT_IN_INTERIOR_CONVEX_HULL
NOT_IN_INTERIOR_CONVEX_HULL_3
NOT_IN_PATH_IMAGE_JOIN
NOT_NEGLIGIBLE_UNIV
NOT_ON_PATH_BALL
NOT_ON_PATH_CBALL
NOT_OUTSIDE_CONNECTED_COMPONENT_LE
NOT_OUTSIDE_CONNECTED_COMPONENT_LT
NOT_SIMPLY_CONNECTED_CIRCLE
NOWHERE_DENSE
NOWHERE_DENSE_UNION
NO_BOUNDED_CONNECTED_COMPONENT_IMP_WINDING_NUMBER_ZERO
NO_BOUNDED_PATH_COMPONENT_IMP_WINDING_NUMBER_ZERO
NO_EMBEDDING_SPHERE_LOWDIM
NO_ISOLATED_SINGULARITY
NO_LIMIT_POINT_IMP_CLOSED
NO_RETRACTION_CBALL
NO_RETRACTION_FRONTIER_BOUNDED
NULLHOMOTOPIC_FROM_CONTRACTIBLE
NULLHOMOTOPIC_FROM_SPHERE_EXTENSION
NULLHOMOTOPIC_INTO_ANR_EXTENSION
NULLHOMOTOPIC_INTO_CONTRACTIBLE
NULLHOMOTOPIC_INTO_RELATIVE_FRONTIER_EXTENSION
NULLHOMOTOPIC_INTO_SPHERE_EXTENSION
NULLHOMOTOPIC_ORTHOGONAL_TRANSFORMATION
NULLHOMOTOPIC_THROUGH_CONTRACTIBLE
NULLSET_RULES
NULLSPACE_INTER_ROWSPACE
NUMSEG_DIMINDEX_NONEMPTY
negligible
netlimit
normball