HOL html

Files Index

Theorems Index

N (theorems)

NABS_NEG
NABS_POS
NADD_ADD
NADD_ADDITIVE
NADD_ADD_ASSOC
NADD_ADD_LCANCEL
NADD_ADD_LID
NADD_ADD_SYM
NADD_ADD_WELLDEF
NADD_ALTMUL
NADD_ARCH
NADD_ARCH_LEMMA
NADD_ARCH_MULT
NADD_ARCH_ZERO
NADD_BOUND
NADD_CAUCHY
NADD_COMPLETE
NADD_DIST
NADD_DIST_LEMMA
NADD_EQ_IMP_LE
NADD_EQ_REFL
NADD_EQ_SYM
NADD_EQ_TRANS
NADD_INV
NADD_INV_0
NADD_INV_WELLDEF
NADD_LBOUND
NADD_LDISTRIB
NADD_LE_0
NADD_LE_ADD
NADD_LE_ANTISYM
NADD_LE_EXISTS
NADD_LE_LADD
NADD_LE_LMUL
NADD_LE_RADD
NADD_LE_REFL
NADD_LE_RMUL
NADD_LE_TOTAL
NADD_LE_TOTAL_LEMMA
NADD_LE_TRANS
NADD_LE_WELLDEF
NADD_LE_WELLDEF_LEMMA
NADD_MUL
NADD_MULTIPLICATIVE
NADD_MUL_ASSOC
NADD_MUL_LID
NADD_MUL_LINV
NADD_MUL_LINV_LEMMA0
NADD_MUL_LINV_LEMMA1
NADD_MUL_LINV_LEMMA2
NADD_MUL_LINV_LEMMA3
NADD_MUL_LINV_LEMMA4
NADD_MUL_LINV_LEMMA5
NADD_MUL_LINV_LEMMA6
NADD_MUL_LINV_LEMMA7
NADD_MUL_LINV_LEMMA7a
NADD_MUL_LINV_LEMMA8
NADD_MUL_SYM
NADD_MUL_WELLDEF
NADD_MUL_WELLDEF_LEMMA
NADD_NONZERO
NADD_OF_NUM
NADD_OF_NUM_ADD
NADD_OF_NUM_EQ
NADD_OF_NUM_LE
NADD_OF_NUM_MUL
NADD_OF_NUM_WELLDEF
NADD_RDISTRIB
NADD_SUC
NADD_UBOUND
NEARBY_INVERTIBLE_MATRIX
NEARNEWMAN_EXISTS
NEARZETA_1
NEARZETA_BOUND
NEARZETA_BOUND_LEMMA
NEARZETA_BOUND_SHARP
NEARZETA_CONVERGES
NEARZETA_CONVERGES_LEMMA
NEARZETA_NONZERO
NEGATED_POLY_ROOT
NEGATIONS_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_SEGMENT_2
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
NEG_ABS
NEG_LAST
NEG_N_IS_INT
NEG_ODD_LEM
NEIGHBOURHOOD_EXTENSION_INTO_ANR
NEIGHBOURHOOD_EXTENSION_INTO_ANR_LOCAL
NEIGHBOURHOOD_RETRACT_IMP_ANR
NEIGHBOURHOOD_RETRACT_IMP_ANR_UNIV
NEMPTY
NEQ
NEQ_MULT_GT_LEM
NEQ_MULT_LT_LEM
NEQ_ODD_LEM
NEST_LEMMA
NEST_LEMMA_UNIQ
NET
NETLIMIT_AT
NETLIMIT_ATREAL
NETLIMIT_WITHIN
NETLIMIT_WITHINREAL
NETLIMIT_WITHIN_INTERIOR
NET_ABS
NET_ADD
NET_CONV_BOUNDED
NET_CONV_IBOUNDED
NET_CONV_NZ
NET_DILEMMA
NET_DIV
NET_INV
NET_LE
NET_MUL
NET_NEG
NET_NULL
NET_NULL_ADD
NET_NULL_CMUL
NET_NULL_MUL
NET_SUB
NET_SUM
NEUTRAL_ADD
NEUTRAL_AND
NEUTRAL_COMPLEX_MUL
NEUTRAL_INT_ADD
NEUTRAL_LIFTED
NEUTRAL_MATRIX_ADD
NEUTRAL_MUL
NEUTRAL_OUTER
NEUTRAL_REAL_ADD
NEUTRAL_REAL_MUL
NEUTRAL_SUMSET
NEUTRAL_VECTOR_ADD
NEWMAN_CONVERGES
NEWMAN_INGHAM_THEOREM
NEWMAN_INGHAM_THEOREM_BOUND
NEWMAN_INGHAM_THEOREM_STRONG
NEWMAN_LEMMA
NINE_POINT_CIRCLE_1
NINE_POINT_CIRCLE_2
NNODE
NOMINIMAL_EQUIV
NONCONSTANT_DEGREE
NONCONSTANT_DIFF_0
NONCONSTANT_DIFF_NIL
NONCONSTANT_DIFF_NORMAL
NONCONSTANT_LENGTH
NONEMPTY_HYPERPLANE_CELL
NONEMPTY_SIMPLE_PATH_ENDLESS
NONNEGATIVE_ABSOLUTELY_INTEGRABLE
NONNEGATIVE_ABSOLUTELY_REAL_INTEGRABLE
NONTRIVIAL_CROSS
NONTRIVIAL_LIMIT_WITHIN
NON_EXTENSIBLE_BORSUK_MAP
NON_MEASURABLE_SET
NOPOINT_LEM
NORMAL
NORMALIZED_INDUCT
NORMALIZED_NORM
NORMALIZED_TAUT
NORMALIZE_EQ
NORMALIZE_LENGTH_MONO
NORMALIZE_PAIR
NORMALIZE_SING
NORMAL_CONS
NORMAL_DEGREE
NORMAL_EXISTS
NORMAL_ID
NORMAL_LAST_LENGTH
NORMAL_LAST_NONZERO
NORMAL_LENGTH
NORMAL_NORMALIZE
NORMAL_PDIFF
NORMAL_PDIFF_LEM
NORMAL_PNEG
NORMAL_RTC
NORMAL_TAIL
NORMAL_TC
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_CLOG_BOUND
NORM_COSSIN
NORM_CPOW_LOWERBOUND
NORM_CPOW_REAL
NORM_CPOW_REAL_MONO
NORM_CPRODUCT
NORM_CR
NORM_CROSS
NORM_CROSS_DOT
NORM_CROSS_MULTIPLY
NORM_CSIN_POW_2
NORM_ELIM_THM
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_KLEINIFY
NORM_KLEINIFY_LT
NORM_KLEINIFY_MOEBIUS_LT
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_POINCARIFY_LT
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
NOTENOUGH_4
NOTIN
NOT_ABSOLUTE_RETRACT_COBOUNDED
NOT_ALL
NOT_AND_IMPLIES_lemma
NOT_AND_IMPLIES_lemma1
NOT_AND_IMPLIES_lemma2
NOT_AND_OR_NOT_lemma
NOT_BOUNDED_UNIV
NOT_CLAUSES_WEAK
NOT_CONG_MINUS1
NOT_CONS
NOT_CONS_NIL
NOT_COPLANAR_0_4_IMP_INDEPENDENT
NOT_COPLANAR_IMP_NOT_COLLINEAR_DROPOUT_3
NOT_COPLANAR_NOT_COLLINEAR
NOT_ELIM2
NOT_EMPTY_INSERT
NOT_EQUAL_SETS
NOT_EVEN
NOT_EVENTUALLY
NOT_EVEN_EQ_ODD
NOT_EX
NOT_EXISTS_CONJ_THM
NOT_EXISTS_TAG
NOT_EXISTS_THM
NOT_EXISTS_UNIQUE_THM
NOT_EXP_0
NOT_FORALL_TAG
NOT_FORALL_THM
NOT_False_lemma
NOT_HYPERPLANE_CELL_EMPTY
NOT_IMPLIES_False_lemma
NOT_IMPLY_OR_lemma
NOT_IMP_EQ_EQ_EQ_OR
NOT_IMP_EQ_OR_EQ_EQ_OR_OR
NOT_INSERT_EMPTY
NOT_INTEGER_DIV_POW2
NOT_INTEGER_LEMMA
NOT_INTERVAL_UNIV
NOT_IN_EMPTY
NOT_IN_INTERIOR_CONVEX_HULL
NOT_IN_INTERIOR_CONVEX_HULL_3
NOT_IN_OWN_RADICALS
NOT_IN_PATH_IMAGE_JOIN
NOT_IN_VARIANT
NOT_IS_RESULT
NOT_LE
NOT_LESS_0
NOT_LT
NOT_MEM_DELETE1
NOT_NEGLIGIBLE_UNIV
NOT_NIL
NOT_NOT_lemma
NOT_ODD
NOT_ON_PATH_BALL
NOT_ON_PATH_CBALL
NOT_OR_AND_NOT_lemma
NOT_OR_IMPLY_lemma
NOT_OUTSIDE_CONNECTED_COMPONENT_LE
NOT_OUTSIDE_CONNECTED_COMPONENT_LT
NOT_POLY_CMUL_NIL
NOT_POLY_EXP_NIL
NOT_POLY_EXP_X_NIL
NOT_POLY_MUL_ITER_NIL
NOT_POLY_MUL_NIL
NOT_PRIME_THM
NOT_PSUBSET_EMPTY
NOT_P_IMPLIES_P_EQ_False_lemma
NOT_ROL
NOT_SIMPLY_CONNECTED_CIRCLE
NOT_SUC
NOT_SUC_LESS_EQ
NOT_TARSKI_AXIOM_10_NONEUCLIDEAN
NOT_TRANSCENDENTAL_ZERO
NOT_True_lemma
NOT_UNIV_PSUBSET
NOT_def1
NOT_def2
NOT_g_NIL
NOVEMBER_LEMMA_1
NOVEMBER_LEMMA_2
NOWHERE_DENSE
NOWHERE_DENSE_UNION
NO_BOUNDED_CONNECTED_COMPONENT_IMP_WINDING_NUMBER_ZERO
NO_BOUNDED_PATH_COMPONENT_IMP_WINDING_NUMBER_ZERO
NO_CONST_TERM_POLY_ROOT
NO_EMBEDDING_SPHERE_LOWDIM
NO_ISOLATED_SINGULARITY
NO_LIMIT_POINT_IMP_CLOSED
NO_PRIMITIVE_ROOT_MODULO_COMPOSITE
NO_PRIMITIVE_ROOT_MODULO_POW2
NO_RETRACTION_CBALL
NO_RETRACTION_FRONTIER_BOUNDED
NPAIR
NPAIR_INJ
NPAIR_INJ_LEMMA
NPAIR_LT
NPAIR_NONZERO
NPRODUCT_CANCEL_PRIME
NPRODUCT_CLAUSES
NPRODUCT_CMUL
NPRODUCT_CONST
NPRODUCT_DELETE
NPRODUCT_DELTA_CONST
NPRODUCT_EQ
NPRODUCT_EQ_1_EQ
NPRODUCT_EQ_GEN
NPRODUCT_INJECTION
NPRODUCT_MOD
NPRODUCT_MULT
NPRODUCT_PAIRUP_INDUCT
NPRODUCT_SPLITOFF
NPRODUCT_SPLITOFF_HACK
NSQRT_2
NSUM_0
NSUM_ADD
NSUM_ADD_GEN
NSUM_ADD_NUMSEG
NSUM_ADD_SPLIT
NSUM_BIJECTION
NSUM_BOUND
NSUM_BOUND_GEN
NSUM_BOUND_LEMMA
NSUM_BOUND_LT
NSUM_BOUND_LT_ALL
NSUM_BOUND_LT_GEN
NSUM_CASES
NSUM_CLAUSES
NSUM_CLAUSES_LEFT
NSUM_CLAUSES_NUMSEG
NSUM_CLAUSES_RIGHT
NSUM_CLOSED
NSUM_CONST
NSUM_CONST_NUMSEG
NSUM_DELETE
NSUM_DELTA
NSUM_DIFF
NSUM_DISTINCT_OF_ODD
NSUM_EQ
NSUM_EQ_0
NSUM_EQ_0_IFF
NSUM_EQ_0_IFF_NUMSEG
NSUM_EQ_0_NUMSEG
NSUM_EQ_GENERAL
NSUM_EQ_GENERAL_INVERSES
NSUM_EQ_NUMSEG
NSUM_EQ_SUPERSET
NSUM_GROUP
NSUM_IMAGE
NSUM_IMAGE_GEN
NSUM_IMAGE_NONZERO
NSUM_INCL_EXCL
NSUM_INJECTION
NSUM_LE
NSUM_LE_NUMSEG
NSUM_LMUL
NSUM_LT
NSUM_LT_ALL
NSUM_MULTICOUNT
NSUM_MULTICOUNT_GEN
NSUM_NSUM_PRODUCT
NSUM_NSUM_RESTRICT
NSUM_OFFSET
NSUM_OFFSET_0
NSUM_PAIR
NSUM_PERMUTE
NSUM_PERMUTE_NUMSEG
NSUM_POS_BOUND
NSUM_POS_LT
NSUM_RESTRICT
NSUM_RESTRICT_SET
NSUM_RMUL
NSUM_SING
NSUM_SING_NUMSEG
NSUM_SUBSET
NSUM_SUBSET_SIMPLE
NSUM_SUPERSET
NSUM_SUPPORT
NSUM_SWAP
NSUM_SWAP_NUMSEG
NSUM_TRIV_NUMSEG
NSUM_UNION
NSUM_UNIONS_NONZERO
NSUM_UNION_EQ
NSUM_UNION_LZERO
NSUM_UNION_NONZERO
NSUM_UNION_RZERO
NTRIE
NTRIE_DECODE_THM
NTRIE_DELETE
NTRIE_DIFF
NTRIE_DISJOINT
NTRIE_EQ
NTRIE_IMAGE
NTRIE_IMAGE_DEF
NTRIE_IN
NTRIE_INSERT
NTRIE_INTER
NTRIE_RELATIONS
NTRIE_SING
NTRIE_SUBSET
NTRIE_UNION
NULL
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
NULLSTELLENSATZ_LEMMA
NULLSTELLENSATZ_UNIVARIATE
NULL_EQ_NIL
NULL_LENGTH
NUM2_COUNTABLE
NUMBER_DENUMBER
NUMBER_INJ
NUMBER_OF_COMBINATIONS
NUMBER_OF_COMBINATIONS_EXPLICIT
NUMBER_OF_DERANGEMENTS
NUMBER_OF_PAIRINGS
NUMBER_OF_PERMUTATIONS
NUMBER_SURJ
NUMERAL
NUMPAIR
NUMPAIR_DEST
NUMPAIR_INJ
NUMPAIR_INJ_LEMMA
NUMSEG_1_CLAUSES
NUMSEG_2
NUMSEG_ADD_SPLIT
NUMSEG_CLAUSES
NUMSEG_COMBINE_L
NUMSEG_COMBINE_R
NUMSEG_DIMINDEX_NONEMPTY
NUMSEG_EMPTY
NUMSEG_LE
NUMSEG_LENGTH_POLYDIFF_LEMMA
NUMSEG_LREC
NUMSEG_LT
NUMSEG_OFFSET_IMAGE
NUMSEG_REC
NUMSEG_RESTRICT_SUC
NUMSEG_RREC
NUMSEG_SING
NUMSUM
NUMSUM_DEST
NUMSUM_INJ
NUM_CASES_LEMMA
NUM_COUNTABLE
NUM_DIVIDES_INT_DIVIDES
NUM_GCD
NUM_INTEGRAL
NUM_INTEGRAL_LEMMA
NUM_INTRO
NUM_LAGRANGE_LEMMA
NUM_OF_INT
NUM_OF_INT_ABS
NUM_OF_INT_OF_NUM
NZERO
N_IS_INT
Noncollinear_2Span
Noncollinear_3ImpliesDistinct
NotMove2ImpliesCollinear
n_nz
n_suc
nabs
nadd_add
nadd_eq
nadd_inv
nadd_le
nadd_mul
nadd_of_num
nadd_rinv
nat_mod
nat_mod_lemma
nc_thm
nearnewman
nearzeta
neg_cont
neg_continuous
neg_dim
neg_neg_neq_thm
neg_neg_neq_thm2
neg_odd_lem
neg_point
neg_pos_neq_thm
neg_pos_neq_thm2
neg_thm_n
neg_thm_p
neg_zero_neg_thm
negatef
negativef
negligible
neigh
neths
netlimit
neutral
newman
next
nmax
nmax_le
no_k33_planar_graph_data
node_INDUCT,node_RECURSION
nonconstant
norm
norm2_0
norm2_bounds
norm2_cis
norm2_nn
norm2_point
norm2_scale
norm2_scale_cis
norm_dot
norm_n
norm_neg
norm_nonneg
norm_scale
norm_scale2
norm_scale_vec
norm_triangle
normal
normal_nonconstant
normalize
normalized
normball
not_cls_exists
not_def
not_eq
not_not
nproduct
nsum
num_Axiom
num_CASES
num_FINITE
num_FINITE_AVOID
num_INDUCTION
num_INFINITE
num_MAX
num_RECURSION_STD
num_SEG_UNION
num_WF
num_WOP
num_above_finite
num_above_infinite
num_abs_of_int0
num_abs_of_int_exists
num_abs_of_int_mono
num_abs_of_int_mul
num_abs_of_int_neg
num_abs_of_int_num
num_abs_of_int_pre
num_abs_of_int_select
num_abs_of_int_suc
num_abs_of_int_th
num_abs_of_int_triangle
num_closure0
num_closure0_edge
num_closure1
num_closure2
num_closure_delete
num_closure_elt
num_closure_mono
num_closure_pos
num_closure_size
num_congruent
num_coprime
num_divides
num_gcd
num_infinite
num_lower_down
num_lower_set
num_mod
num_of_int
number
numeral
numseg