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 | _ |
I (theorems)
IMAGE2IMAGE_I
IMAGE_INTERS
IMAGE_SURJ
INFINITE_PIGEONHOLE
INJ_IMAGE
INJ_UNIV
INTERS_EMPTY
INTERS_EQ_EMPTY
INTERS_SUBSET
INTERS_SUBSET2
INTERVAL_0
INTERVAL_ABSV
INTERVAL_ABS_MAX
INTERVAL_ABS_MIN
INTERVAL_ADD
INTERVAL_CENTER
INTERVAL_DIV
INTERVAL_EPS_0
INTERVAL_EPS_POS
INTERVAL_MAX
INTERVAL_MIN
INTERVAL_MINMAX
INTERVAL_MK
INTERVAL_MUL
INTERVAL_NEG
INTERVAL_NEG2
INTERVAL_NUM
INTERVAL_OF_TWOPOW
INTERVAL_SSQRT
INTERVAL_SUB
INTERVAL_TO_LESS
INTERVAL_WIDTH
INTER_FINITE
INTER_THM
INT_ABS_NEG_NUM
INT_ABS_NUM
INT_ADD_NEG
INT_ADD_NEG_NUM
INT_ADD_NEGv2
INT_IS_INT
INT_NN_NEG
INT_NUM
INT_NUM_REAL
INT_OF_NUM_DEST
INT_POS'
INT_POS_NEG
INT_POW_EVEN_NEG1
INT_POW_MUL
INT_POW_NEG1
INT_POW_ODD_NEG1
INT_POW_POW
INT_REP
INT_REP2
INT_REP3
INT_SUB
INT_ZERO
INT_ZERO_NEG
INVERSE_BIJ
INVERSE_DEF
INVERSE_FN
INVERSE_XY
INV_homeomorphism
I_BIJ
image_app
image_compact
image_curve_cell_reflA
image_curve_cell_reflB
image_curve_cell_reflC
image_delete_choice
image_domain_sub
image_empty
image_imp
image_inj
image_interval
image_interval2
image_inv_image
image_power_inj
image_power_surj
image_powerset
image_preimage
image_sing
image_top
image_unions
in_pair
in_preimage
in_union
incf_V
incf_value
induced_compact
induced_top_interval
induced_top_open
induced_top_support
induced_top_top
induced_top_unions
induced_trans
inductive_diff
inductive_inter
inductive_segment
inductive_set_adj
inductive_set_endpoint
inductive_set_join
inductive_set_restrict
inductive_univ
inf_LB
inf_eps
inf_unique
infinite_closed_interval
infinite_image
infinite_int
infinite_interval
infinite_intpair
infinite_subset
inj_bij
inj_bij_size
inj_domain_sub
inj_image_subset
inj_inter
inj_split
inj_subset
inj_subset2
inj_subset_domain
inj_terminal
insert_sing
int2_range_finite
int_arch
int_le_mp
int_lt_suc_le
int_neg_num_th
int_pow2_gt1
int_range_finite
int_suc
integer_cube_finite
inter_lattice
inter_midpoint
inter_union
inters_inter
inters_singleton
inters_subset
interval
interval_closed
interval_closed_ball
interval_compact
interval_eq
interval_euclid1_bounded
interval_euclid1_closed
interval_euclid1_compact
interval_finite
interval_image
interval_subset
inv_comp_left
inv_comp_right
inv_twopow
invo_BIJ
invo_homeo
iso_eps_support0
iso_int_model_lemma
iso_support_eps_finite
iso_support_eps_min
iso_support_eps_nonempty
iso_support_min_int
isthree