HOL html

Files Index

Theorems Index

N (theorems)

NABS_NEG
NABS_POS
NEGLIGIBLE_AFF_3
NEGLIGIBLE_AFF_3_FAN
NEGLIGIBLE_AFF_3_INTER_BALL
NEGLIGIBLE_AFF_3_UNION_INTER_BALL
NEGLIGIBLE_AFF_GE_1_2
NEGLIGIBLE_AFF_GE_2_1
NEGLIGIBLE_AFF_GT_1_2
NEGLIGIBLE_AFF_GT_1_2_INTER_BALL
NEGLIGIBLE_FUNC
NEGLIGIBLE_INTER_VORONOI_CLOSED
NEGLIGIBLE_MEASURE_UNION_klema
NEGLIGIBLE_XFAN
NEGLIGIBLE_XFAN_INTER_BALL
NEG_SIGNS_LEMMA
NEHXMWH
NEIGHBORHOOD_lemma
NETLIMIT_WITHIN_FAN
NET_DILEMMA_FAN
NET_FAN
NEUTRAL_VECTOR_ADD
NEVER_USED_AGAIN
NEXT_EL
NEXT_EL_ALT
NEXT_EL_APPEND_lemma
NEXT_EL_LIST_PAIRS
NEXT_EL_MOD
NEXT_EL_ORBIT
NEXT_EL_POWER
NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT
NEXT_OPOSITE_POINT_IS_NOT_IN_AFF_GT2
NEXT_PREV_ID
NEXT_PRO_IMP_ALLS
NEXT_PRO_IMP_ALLS_STRICT
NGAY23_THANG2_09
NGAY_23_THANG1
NHCXLRV
NHCXLRV_ALT
NHSJMDH
NJIUTIU
NKEZBFC
NKEZBFC_PREP
NLVWBBW
NN_OF_HYP_EQ
NN_OF_HYP_EQ1
NN_OF_HYP_HAS_ORDERS
NN_OF_HYP_NOT_EQ_ID
NN_OF_HYP_POWER_EQ_ID
NN_OF_HYP_POWER_IDE
NN_OF_HYP_POWER_IN_ORD_PAIRS
NODES_HYPERMAP_OF_LIST_ALL
NODES_OF_LIST
NODE_EDGE_COMM_LEMMA
NODE_FINITE
NODE_HYPERMAP_OF_FAN
NODE_HYPERMAP_OF_FAN_ALT
NODE_HYPERMAP_OF_FAN_POWER_MAP_POINTS
NODE_HYPERMAP_OF_FAN_lemma
NODE_HYPERMAP_OF_LIST_EXPLICIT
NODE_MAP_SYM_0
NODE_NOT_EMPTY
NODE_OF_LIST_LEMMA
NODE_OF_SIZE_2
NODE_POWER_MAP_SYM_0
NODE_SET_AS_IMAGE
NODE_SUBSET_DART1_OF_FAN
NODE_SUBSET_DART_OF_FAN
NODE_SY_NOT_ID
NODE_SY_POWER_ID
NODE_TYPE_lemma
NONCOPLANAR_3_BASIS
NONCOPLANAR_4_DISTINCT
NONLIN
NONPARALLEL_BALL_ANNULUS
NONPARALLEL_BALL_ANNULUS362
NONPARALLEL_BALL_ANNULUS40
NONPARALLEL_BALL_ANNULUS40_ALT
NONPARALLEL_BALL_ANNULUS_ALT
NONPLANAR_OPEN
NON_ZERO
NORM1_NOT_0
NORM1_NZ
NORMBALL_SUBSET
NORM_0
NORM_BASIS
NORM_BASIS_1
NORM_BASIS_VEC3
NORM_BOUND_COMPONENT_LE
NORM_BOUND_COMPONENT_LT
NORM_BOUND_GENERALIZE
NORM_BOUND_LEMMA_FAN
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_CAUCHY_SCHWARZ_FRAC
NORM_CAUCHY_SCHWARZ_FRAC2
NORM_COS_ANGLE_4POINT
NORM_COS_ANGLE_LE
NORM_COS_ANGLE_LT
NORM_CROSS
NORM_CROSS_LE
NORM_CROSS_MULTIPLY
NORM_CROSS_PRODUCT_UPS_X
NORM_EQ
NORM_EQ_0
NORM_EQ_0_DOT
NORM_EQ_0_IMP
NORM_EQ_1
NORM_EQ_SQUARE
NORM_FLATTEN
NORM_FSTCART
NORM_GE_SQUARE
NORM_GT_SQUARE
NORM_LE
NORM_LE_0
NORM_LE_2_IN_BBS
NORM_LE_2_IN_MMS
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_PASTECART
NORM_PASTECART_LE
NORM_POS_COLLINEAR
NORM_POS_LE
NORM_POS_LT
NORM_POW2_SUM2
NORM_POW_2
NORM_PROJECTION_LE
NORM_REAL
NORM_SCALING
NORM_SNDCART
NORM_SUB
NORM_TRIANGLE
NORM_TRIANGLE_EQ
NORM_TRIANGLE_LE
NORM_TRIANGLE_LT
NORM_TRIANGLE_SUB
NORM_VECMAT
NORM_VECMAT_SUM
NORM_VECTOR2_TRIG
NORM_V_IN_BB_LE_CSTAB
NOT_0_IMP_SUM_CHI_1
NOT_2EQ_IMP_SIN_ARCV
NOT_BASISES_EQ_VEC0
NOT_CIRCULAR_SY
NOT_COLLINEAR
NOT_COLLINEAR_AFF_DIM2
NOT_COLLINEAR_AFF_DIM_2
NOT_COLLINEAR_BBs_CASE_3
NOT_COLLINEAR_IMP_CROSS_NOT_COPLANAR
NOT_COLLINEAR_IMP_DIHV_BOUNDED
NOT_COLLINEAR_IMP_NOT_SIN0
NOT_COLLINEAR_IMP_UPS_LT
NOT_COLLINEAR_SYM_0
NOT_COLL_IMP_COPL
NOT_COLL_IMP_NOT_AFF_SUB
NOT_COLL_IMP_POS_SUM
NOT_COLL_IMP_RADV_FORMULAR
NOT_COLL_IMP_ZERO_DETER
NOT_COLL_IM_SIN_LT
NOT_COLL_ORTHONORMAL
NOT_COLL_RHONODE_SND_POINT
NOT_COL_AND_ORTHO_IMP_NOT_COPL
NOT_COL_EQ_UPS_X_POS
NOT_COL_IMP_RADV
NOT_COL_IMP_RADV_PROPERTIY
NOT_COPLANAR_0_4_IMP_INDEPENDENT
NOT_COPLANAR_AFF_3
NOT_COPLANAR_AND_SUM_IMP_UNIQUE
NOT_COPLANAR_EXTREME_MCELL2
NOT_COPLANAR_IMP_CARD4
NOT_COPLANAR_IMP_CARD4_ALT
NOT_COPLANAR_IMP_EXISTS_CIR
NOT_COPLANAR_IMP_RADV_PROPERTIES
NOT_COPLANAR_OMEGA_LIST_N
NOT_COPLANAR_R3
NOT_CO_IMP_DIST_POS
NOT_EMPETY_MMS_TRANSFER
NOT_EMPTY_BBs_v39
NOT_EMPTY_CASE_3
NOT_EMPTY_CASE_3_IS_SCS
NOT_EMPTY_CASE_4
NOT_EMPTY_CASE_4_3
NOT_EMPTY_CASE_4_IS_SCS
NOT_EMPTY_CASE_4_sqrt8
NOT_EMPTY_CASE_5
NOT_EMPTY_CASE_5_IS_SCS
NOT_EMPTY_CASE_5_pro_cs
NOT_EMPTY_CASE_5_sqrt8
NOT_EMPTY_CASE_6
NOT_EMPTY_CASE_6_IS_SCS
NOT_EMPTY_IMAGE
NOT_EMPTY_SYM_0
NOT_EMP_INJ_IMP_SURJ
NOT_EQ0_IMP_NEITHER_INVERT
NOT_EQ0_IMP_TRIGIZABLE
NOT_EQ_DIAG
NOT_EQ_IMPCOS_ARC
NOT_EQ_IMP_AFF_AND_COLL3
NOT_EQ_IMP_EXISTS_BASIC
NOT_EQ_IMP_TOTAL_ORDER
NOT_EQ_VEC0_IMP_EQU_AFF_COLL
NOT_EXISTS_TAG
NOT_FORALL_TAG
NOT_IDEN_IMP_ABS_LE
NOT_ID_IMP_EXISTS_MAX_EQ_TRUNCATE_SIMPLEX
NOT_ID_IMP_LISTS_NOT_EQ
NOT_IMP_SUC_MOD_EQ
NOT_INTERSECTION_BWT_AFF_GTS
NOT_INTER_EQ_EM_IMP_AFF_SUBSET
NOT_IN_DART1_OF_FAN
NOT_IN_DARTS_NN_IDE
NOT_IN_DARTS_NN_OF_HYP_POWER_IDE
NOT_IN_DART_IMP_IDE
NOT_IN_SYSTEM
NOT_MOD_4_CASES
NOT_MOD_4_CASES_3
NOT_QY_LEM
NOT_STR_IN_CASES_4
NOT_STR_IN_CASES_4_1
NOT_SUBSET_EMPTY_SYM_0
NOT_TOW_EQ_IMP_COL_EQUAVALENT
NOT_UPS_X_EQ_0_IMP
NOT_UPS_X_ZERO_IMP_SMT
NOT_VEC0_IMP_LE1
NOT_VEC0_UNITABLE
NOT_X_IN_AFF_X_A
NOT_ZERO_EQ_POW2_LT
NOV1
NOV10
NOV10'
NOV11
NOV2
NOV20
NOV21
NOV6
NOV7
NOV9
NOVE21
NOVE30
NOVE31
NO_4CELL_IMP_K3
NO_IS_EAR
NO_IS_EAR_SCS_OPP
NSUM_EQ_0_IFF
NULLSET_AFF_2_1
NULLSET_DIFF
NULLSET_INTER
NULLSET_MCELL1
NULLSET_SPHERE
NULLSET_SUBSET
NULLSPACE_INTER_ROWSPACE
NULL_SDIFF_TRANS
NULL_SERIES_1
NUM1_GENERIC
NUM2_COUNTABLE
NUMERAL_EQ
NUMSEG_012
NUMSEG_2
NUMSEG_3
NUMSEG_DIMINDEX_NONEMPTY
NUMSEG_INTER_22
NUMSEG_LT
NUMSEG_SET_VER
NUMSEG_SUBSET_INDUCT
NUM_COUNTABLE
NUM_EXP_0
NUM_EXP_ADD
NUM_EXP_DIV1
NUM_EXP_DIV2
NUM_EXP_EQ_0
NUM_EXP_EXP
NUM_EXP_LE
NUM_EXP_LE1
NUM_EXP_LE1_EQ
NUM_EXP_LE2
NUM_EXP_LE2_EQ
NUM_EXP_LT
NUM_EXP_LT1
NUM_EXP_LT1_EQ
NUM_EXP_LT2
NUM_EXP_LT2_EQ
NUM_EXP_MUL
NUM_EXP_SUB1
NUM_EXP_SUB2
NUM_EXP_SUB_lemma
NUM_EXP_SUM
NUM_EXP_SUM1
NUM_EXP_n0
NUM_FINITE_IMP_MAX_EXISTS
NUM_INTRO
NUM_REMOVE
NUM_THM
NUM_ZERO
NUNRRDS_0
NUNRRDS_1
NUXCOEA
NUXCOEAv2
NWDGKXH
NWVRFMF
NZ_IMP_NORM1
N_EQ_E_FI
N_FAN
N_FAN_EQ_0_IMP_CARD_FACE_EQ_3
N_FAN_GE_0
N_FAN_PAIR_EXT
N_FAN_PAIR_EXT_IN_DART1_OF_FAN
N_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN
N_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN
N_FAN_PAIR_EXT_POWER
N_HYP_TO_AZIM_CYCLE_LEM
N_LIST_EXT_FST
N_LIST_EXT_PERMUTES_DARTS
N_LT_SUC
n_fan
n_fan_pair
n_fan_pair_ext
n_fan_permutes
n_fan_permutes_prime
n_hyp_of_fan
n_list
n_list_ext
n_of_hyp
nabs
ncons
near
near2t0
negligible_cube
negligible_fun_0
negligible_fun_any_C
negligible_fun_p
negligible_voronoi
neq_elim_th
netlimit_fan
new_fan
new_graph_th
next
next_and_loop_darts
next_el
next_head_outside_atom
ngu
nilp
nmap_permute
nmap_via_choice
nn_of_hyp
nn_of_hyp2
nn_of_hyp3
nn_of_hyp_elim
no_loops
no_origin_aff_ge_is_aff_gt
node
node2_y
node3_y
node_contour
node_cyclic_map_lemma
node_deform
node_degenerate_walkup_edge_map
node_degenerate_walkup_node_map
node_exceptional_face
node_exterior_contour
node_fan
node_fan_character
node_fan_map
node_interior_contour
node_lbound_lm
node_map
node_map_and_darts
node_map_face_walkup
node_map_free_loop
node_map_injective
node_map_inverse_representation
node_map_node_walkup
node_map_of_fan
node_map_on_margin
node_map_walkup
node_path
node_refl
node_set
node_subset_dart_fan
node_type_exceptional_face
node_walkup
nodes_of_list
non_collinear_lemma
non_empty_cinterval
non_fixed_point_lemma
nonconformin_fan_imp_exist_3point_in_face
nonconformin_fan_imp_exist_face_gt_3
nonconformin_fan_imp_n_fan_ge0
nonempty_cube
nonf_gamma23_erase126_x
nonf_gamma23_full8_x
nonf_gamma23_keep135_x
nonf_gamma2_x1_div_a
nonf_gamma2_x1_div_a_v2
nonf_gamma3_x
nonf_gamma3f_x_div_sqrt_delta
nonf_gamma3f_x_div_sqrtdelta
nonf_truncate_gamma23_x
nonf_truncate_gamma23_x_B
nonf_truncate_gamma23_x_C
nonf_truncate_gamma3f_x
nonf_truncate_sol_x
nonf_truncate_vol3f
nonf_truncate_vol3r_456
nonf_truncate_vol_x
nonf_ups_126
nonfunctional_edge2_126_x
nonfunctional_edge2_135_x
nonfunctional_edge2_234_x
nonfunctional_flat_term2_126
nonfunctional_flat_term2_135
nonfunctional_flat_term2_234
nonfunctional_mu6_x
nonfunctional_mudLs_126
nonfunctional_mudLs_135
nonfunctional_mudLs_234
nonfunctional_mud_126
nonfunctional_mud_135
nonfunctional_mud_234
nonfunctional_taud_D1
nonfunctional_taud_D2
nonsetedge_fully_surround_fan
norm1_cauchy_eq
norm2hh
norm2hh_x
norm_dot_fan
norm_ineq_lt
norm_lemma1
norm_lemma2
norm_mul_normalize
norm_normalize
norm_of_normal_vector_is_unit_fan
norm_origin_fan
normal
normal_face_collection
normal_lemma1
normal_lemma2
normalize
normalize_vec_0
normalizer
normball
normball_ellip0
normball_eq
normball_subset
normize
not_azim_points1_in_yfan
not_azim_points2_in_yfan
not_azim_points_in_yfan
not_collinear_is_properties_fully_surrounded
not_collinear_is_properties_fully_surrounded1
not_cut_in_edges_fan
not_cut_inside_fan
not_empty_rcone_fan_inter_aff_gt
not_empty_rw_dart_fan
not_in_set3
not_in_set_of_edge
not_in_voronoi
not_open
not_open_voronoi1
not_open_voronoi2
not_open_voronoi3
notcoplanar_4point_aff_gt_1_3_not_empty
notcoplanar_4point_aff_gt_3_1_not_empty
notcoplanar_disjoint
notcoplanar_disjoints
notcoplanar_imp_notcollinear_fan
notempty_xfan_inter_segment_fan
notzerodenom
notzerodenom2
nseq
nth
nth_derivative
nth_diff2_pow
nth_diff_strong
nth_diff_strong_int
nth_diff_weak
nth_differentiable
nth_differentiable_on
nth_differentiable_on_int
nua_kg
nua_kg_version2
null_equiv
num1
num1_poly
num2
num_SEG_UNION
num_above_finite
num_above_infinite
num_cases
num_combo1
num_exp
num_infinite
num_seq_exists
num_y
number_of_components
number_of_edges
number_of_exceptional
number_of_faces
number_of_nodes
number_of_orbits
number_of_orbits_fan
number_of_quadrilateral
number_of_triangle
numm0