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)
NABS_NEGNABS_POS
NOT_EXISTS_TAG
NOT_FORALL_TAG
NUM2_COUNTABLE
NUM_COUNTABLE
NUM_INTRO
nabs
neg_cont
neg_continuous
neg_dim
neg_point
no_k33_planar_graph_data
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
not_cls_exists
not_eq
not_not
num_SEG_UNION
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_infinite
num_lower_down
num_lower_set