HOL html

Files Index

Theorems Index

I (theorems)

IBZWFFH
IDBEZAL
IDENTIFY_AZIM_CYCLE
IDENTIFY_AZIM_CYCLE_SIMPLE
IDENT_WHEN_IDENT_SIN_COS
IDE_ON_S_IMP_SAME_IMAGE
ID_FF_OF_HYP_NOT_DARTS
ID_NN_OF_HYP_NOT_DARTS
ID_PAIR_SYM_0
ID_SYM_0
ID_SYM_0_PRIME
IK_SY
IMAGE_4_EXPLICIT
IMAGE_BBINDEX_SYM_0
IMAGE_DROP_UNIV
IMAGE_E_SYM_0
IMAGE_E_UNION_V_SYM_0
IMAGE_F1_IN_FACE_IMP_IN_FACE
IMAGE_F1_POWER_IN_FACE_IMP_IN_FACE
IMAGE_FACE_F
IMAGE_FF
IMAGE_INTER_AFF3
IMAGE_LEMMA
IMAGE_LIFT_DROP
IMAGE_LIFT_UNIV
IMAGE_NN_OF_HYP_EQ_F_SY
IMAGE_NN_OF_HYP_F_SY
IMAGE_NODE_SYM_0
IMAGE_NUMSEG222
IMAGE_SEG
IMAGE_SUBSET_IN
IMAGE_SURJ
IMAGE_V_SYM_0
IMAGE_WW_DEFOR
IMJXPHR
IMJXPHRv2
IMPLY_POS
IMP_A1_EQ_0
IMP_AFFINE_HULL_SUBSET
IMP_ETAY_POS
IMP_FAN_V_PRIME_E_PRIME
IMP_GT_THAN_TWO
IMP_IN_AFF4
IMP_IN_AFF_LT
IMP_IN_BA
IMP_IN_Q_SYS
IMP_NORM_FAN
IMP_OTHO4
IMP_OTHORGONAL_AFF3
IMP_PRE_LE_19
IMP_PROPERTIES_OF_CIR4
IMP_QUA
IMP_QUA_RE_TE
IMP_SUC_MOD_EQ
IMP_SUC_MOD_EQ1
IM_UP_POS
IN1
IN1_ORBITS_FAN
IN2
IN2_ORBITS_FAN
INDENT_IN_S1_IMP_BIJ
INDEPENDENT_2
INDEPENDENT_3
INDEPENDENT_BOUND
INDEPENDENT_BOUND_GENERAL
INDEPENDENT_CARD_LE_DIM
INDEPENDENT_EMPTY
INDEPENDENT_EXPLICIT
INDEPENDENT_EXPLICIT_NUMSEG
INDEPENDENT_IMP_FINITE
INDEPENDENT_INJECTIVE_IMAGE
INDEPENDENT_INJECTIVE_IMAGE_GEN
INDEPENDENT_INSERT
INDEPENDENT_LINEAR_IMAGE_EQ
INDEPENDENT_MONO
INDEPENDENT_NONZERO
INDEPENDENT_SPAN_BOUND
INDEPENDENT_STDBASIS
INDEX
INDEX_EL
INDEX_EQ_LENGTH
INDEX_FST_SND
INDEX_HD
INDEX_J1_SY
INDEX_J1_TS
INDEX_LE_LENGTH
INDEX_LT_LENGTH
INDEX_VECMAT
INDUCTION_FANADD
INEQ_ALT
INFINITE_CRIT
INFINITE_EXISTS
INFINITE_PIGEONHOLE
INFNORM_0
INFNORM_EQ_0
INFNORM_LE_NORM
INFNORM_MUL
INFNORM_MUL_LEMMA
INFNORM_NEG
INFNORM_POS_LE
INFNORM_POS_LT
INFNORM_SET_IMAGE
INFNORM_SET_LEMMA
INFNORM_SUB
INFNORM_TRIANGLE
INITIAL_SUBLIST
INITIAL_SUBLIST_2
INITIAL_SUBLIST_APPEND
INITIAL_SUBLIST_APPEND_2
INITIAL_SUBLIST_APPEND_SING
INITIAL_SUBLIST_CONS
INITIAL_SUBLIST_EXISTS
INITIAL_SUBLIST_EXISTS_ALT
INITIAL_SUBLIST_HD
INITIAL_SUBLIST_HEAD_EQ
INITIAL_SUBLIST_HEAD_EQ_2
INITIAL_SUBLIST_IMP_TRUNCATE_SIMPLEX
INITIAL_SUBLIST_INJ
INITIAL_SUBLIST_LENGTH_LE
INITIAL_SUBLIST_NIL
INITIAL_SUBLIST_OF_NIL
INITIAL_SUBLIST_REFL
INITIAL_SUBLIST_SING
INITIAL_SUBLIST_TAIL
INITIAL_SUBLIST_TRANS
INITIAL_SUBLIST_TRUNCATE
INITIAL_SUBLIST_UNIQUE
INJECTIVE_SCALING
INJ_ALT
INJ_BIJ_IMAGE
INJ_B_SY
INJ_CARD
INJ_EDGES_FACE_pr23
INJ_EXTENSION
INJ_FINITE_EXISTS
INJ_IFF_SURJ
INJ_IMAGE
INJ_IMP_BIJ_IMAGE
INJ_IMP_RES_INVERSE
INJ_ROW_B_SY
INJ_SURJ
INJ_TRANF_FACE_DELETE_DS
INJ_TRAN_D1_FAN
INSERT_EMPTY_SUBSET
INSERT_SUBSET
INSERT_UNION_CLAUSES
INTEGER_DET
INTEGER_PRODUCT
INTEGER_SIGN
INTERGRAL_UNIONS_INTERVALS
INTERIOR_AFFINIE_HUL_EQ_UNIV
INTERIOR_AGL_EQ
INTERIOR_ANGLE1_AZIM
INTERIOR_ANGLE1_POS
INTERIOR_ANGLE_LEM_SLICING_FAN
INTERIOR_ANGLE_LEM_SLICING_FAN2
INTERIOR_ANGLE_SAME_V3_DEFOR1
INTERIOR_ANGLE_SAME_V3_DEFOR1_MK
INTERIOR_ANGLE_SAME_V3_DEFOR1_MK_TWO_CASES
INTERIOR_ANGLE_SAME_V3_DEFOR1_TWO_CASES
INTERIOR_ANGLE_SAME_WW_DEFOR
INTERIOR_ANGLE_SAME_WW_DEFOR0
INTERIOR_ANGLE_SAME_WW_DEFOR1
INTERIOR_BIS_LE
INTERIOR_CBALL_FAN
INTERIOR_CLOSURE_FAN
INTERIOR_EQUIVALENT
INTERIOR_EQ_FAN
INTERIOR_IMP_RELATIVE_INTERIOR
INTERIOR_INTERIOR_FAN
INTERIOR_MAXIMAL_FAN
INTERIOR_OPEN_FAN
INTERIOR_SUBSET_FAN
INTERIOR_UNIQUE_FAN
INTERIOR_VORONOI_CLOSED
INTERIOR_VORONOI_CLOSED_INTERIOR
INTERSECTION_LEMMA
INTERS_2_LEMMA
INTERS_EMPTY
INTERS_HALF_SPACE_DS_FANADD1
INTERS_HALF_SPACE_DS_FANADD2
INTERS_HALF_SPACE_DS_FANADD3
INTERS_INTER_INTERS
INTERS_INTER_INTERS_ALT
INTERS_SUBSET
INTERS_SUBSET2
INTERS_UNIV
INTERVAL_0
INTERVAL_ABSV
INTERVAL_ABS_MAX
INTERVAL_ABS_MIN
INTERVAL_ADD
INTERVAL_CENTER
INTERVAL_DIV
INTERVAL_DIVIDE_Euler_lemma
INTERVAL_EPS_0
INTERVAL_EPS_POS
INTERVAL_FLOAT
INTERVAL_HI
INTERVAL_INV
INTERVAL_INV_NEG
INTERVAL_INV_POS
INTERVAL_LO
INTERVAL_MAX
INTERVAL_MIN
INTERVAL_MINMAX
INTERVAL_MK
INTERVAL_MUL
INTERVAL_MUL_lemma
INTERVAL_MUL_lemma2
INTERVAL_NEG
INTERVAL_NEG2
INTERVAL_NUM
INTERVAL_OF_TWOPOW
INTERVAL_REAL_POW_0
INTERVAL_REAL_POW_1
INTERVAL_SQRT
INTERVAL_SSQRT
INTERVAL_SUB
INTERVAL_TO_LESS
INTERVAL_WIDTH
INTER_2_WEDGE_GE_SUBSET_UNION_2_AFF_GE_LEMMA
INTER_AFFINE_HULL
INTER_AFF_GT_LT_IMP_INTER_AFF_CONV0
INTER_FINITE
INTER_INTERS
INTER_RCONE_GE_IMP_BETWEEN_PROJ_POINT
INTER_RCONE_GE_LE_lemma
INTER_RCONE_GE_LT_lemma
INTER_SLICE_SCS_EMPTY
INTER_SLICE_SCS_EMPTY1
INTER_SYM_0
INTER_VORONOI_SUBSET_BISECTOR
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
INVARANT_SIGMA_FAN_ADD
INVERSE1_SIGMA_FAN
INVERSE1_SIG_AND_SIG
INVERSE_ADD_EXPONENTS
INVERSE_BIJ
INVERSE_DEF
INVERSE_EVALUATION
INVERSE_EXISTS_IMP_BIJECTIVE
INVERSE_FACE_CYCLE
INVERSE_FACE_CYCLE_ALL
INVERSE_FACE_EQ_INV_FACE_LOCALLIZED
INVERSE_FN
INVERSE_FUNCTION_OF_BIJ
INVERSE_F_FAN_PAIR_EXT
INVERSE_F_FAN_PAIR_EXT_EXPLICIT
INVERSE_F_IN_DART1_OF_FAN
INVERSE_F_LIST_EXT_LEMMA
INVERSE_LEMMA
INVERSE_PERMUTES
INVERSE_POWER_EVALUATION
INVERSE_POWER_MAP
INVERSE_SIGMA_FAN
INVERSE_SIGMA_FAN_EQ_INVERSE1_SIGMA_FAN
INVERSE_XY
INVERTIBLE_DET_NZ
INVERTIBLE_LEFT_INVERSE
INVERTIBLE_RIGHT_INVERSE
INVERT_NORM_POS_LE
INVS_IN_AFF_GT
INV_ARCLENGTH
INV_AZIM_CYCLE_EQ
INV_AZIM_CYCLE_EQ1
INV_EQ_DIV_LEMMA
INV_INEQUAL_GENERAL
INV_INVERSE
INV_ISO
INV_MULT_POW
INV_VNI
IN_2_2_IMP_CONVEX_HULL_4
IN_AFFINE_HULL_3_KY_LEMMA2
IN_AFFINE_HULL_IMP_COLLINEAR
IN_AFFINE_HULL_KY_LEMMA3
IN_AFFINE_HULL_KY_LEMMA3_alt
IN_AFFINE_KY_LEMMA1
IN_AFF_EQ_DOT_E2_FAN
IN_AFF_GE_CON
IN_AFF_GE_INTERPRET_TO_AFF_GT_AND_AFF
IN_AFF_GT_IMP_AZIMEQ
IN_AFF_HULL_3
IN_AFF_LT_IMP_IN_CONV
IN_AFF_LT_STILL_NOT_COLLINEAR
IN_A_PERIOD_IDE0
IN_BALL_FAN
IN_BAR_DISTINCT
IN_BA_IM_PA_SU
IN_BBPRIME_SUBDIVISION
IN_BBPRIME_SUBDIVISION1
IN_BBPRIME_SUBDIVISION_C_EQ_AM
IN_B_SY1_COLLINEAR_CASE_3
IN_B_SY1_COLLINEAR_CASE_3_IS_SCS
IN_B_SY2_COVER
IN_B_SY_COVER
IN_CBALL_FAN
IN_CONV0
IN_CONV03_EQ
IN_CONV0_AFF_SUBSET
IN_CONV0_EQ_EQ
IN_CONV0_IMP_AFF_EQ
IN_CONV0_IMP_AFF_EQ1
IN_CONV0_IMP_AZIM_PI
IN_CONV0_IMP_AZIM_PI_ALT
IN_CONV0_IMP_COLL_ENDS_AFF
IN_CONV0_IMP_COLL_IFF
IN_CONV3_EQ
IN_CONV_COLLINEAR
IN_CONV_LINE_SEPERATABLE
IN_D1_FAN_IMP_EDGE_FAN
IN_DART1_OF_FAN
IN_DART1_OF_FAN_IMP_CARD_FACE_GT_1
IN_DARTS_EXTENSION
IN_DARTS_FF_IMP_DARTS_E_PRIME_V_PRIME
IN_DARTS_HYP_IMP_FST_SND_IN_V
IN_DARTS_IFF_NN_OF_HYP_TOO
IN_DART_OF_FAN
IN_DART_PRESERVED
IN_DIMINDEX_SWAP
IN_DIRECTION_FAN
IN_DOUBLE
IN_EDGES0_FAN
IN_EE_IFF_IN_E
IN_EQ_PAIR_SYM_0
IN_ESTD
IN_E_IFF_IN_ORD_E
IN_E_IMP_IMP_IN_DARTS
IN_FACE_IMP_IN_DART1_OF_FAN
IN_FACE_IMP_SUBSET_FACE
IN_FF_FACE_MAP_IDE
IN_FF_IMP_AZIM_CYCLE_EQ
IN_FF_IMP_FST_SND_IN_V
IN_HULL_INSERT
IN_IMAGE_LIFT_DROP
IN_IMAGE_VV
IN_INTERIOR_CBALL_FAN
IN_INTERIOR_FAN
IN_INTERVAL_1
IN_INTERVAL_FAN
IN_IS_SCS_CASE_3
IN_IS_SCS_CASE_4
IN_IS_SCS_CASE_5
IN_IS_SCS_CASE_6
IN_J_IMP_IN_J1_SY
IN_NODE_IMP_FIRST_EQ
IN_NOT_EMPTY_B1_SY_3
IN_NOT_EMPTY_B1_SY_3_IS_SCS
IN_NOT_EMPTY_B1_SY_4
IN_NOT_EMPTY_B1_SY_4_3
IN_NOT_EMPTY_B1_SY_4_IS_SCS
IN_NOT_EMPTY_B1_SY_4_sqrt8
IN_NOT_EMPTY_B1_SY_5
IN_NOT_EMPTY_B1_SY_5_IS_SCS
IN_NOT_EMPTY_B1_SY_5_pro_cs
IN_NOT_EMPTY_B1_SY_5_sqrt8
IN_NOT_EMPTY_B1_SY_6
IN_NOT_EMPTY_B1_SY_6_IS_SCS
IN_NOT_EMPTY_CASE_3
IN_NOT_EMPTY_CASE_4
IN_NOT_EMPTY_CASE_4_3
IN_NOT_EMPTY_CASE_4_sqrt8
IN_NOT_EMPTY_CASE_5
IN_NOT_EMPTY_CASE_5_pro_cs
IN_NOT_EMPTY_CASE_5_sqrt8
IN_NOT_EMPTY_CASE_6
IN_OPOSITE_SIDE_IMP_INTER
IN_ORBITS_FAN
IN_ORBIT_IMP_ORBIT_SUBSET
IN_ORBIT_MAP_IMP_F_Y
IN_ORD_E_EQ_IN_E
IN_ORD_E_IFF_SWITCH_TOO
IN_ORD_PAIRS_E_PRIME
IN_ORD_PAIRS_IMP_IMP_IN_TOO
IN_ORD_PAIRS_IMP_NN_OF_HYP_IN_ORD
IN_ORD_PAIRS_IMP_SND_IN_EE_FST
IN_ORIGIN_PERIOD_IMP_UNIQUENESS
IN_PAIR_SYM_0
IN_PLANE_IMP_OTHORGONAL
IN_PLANE_NOT_COLLINEAR
IN_P_HULL_INSERT
IN_Q_IMP
IN_Q_IMP_BAR
IN_Q_SYS_IMP4
IN_RELATIVE_INTERIOR1
IN_SCS_STR_CASES_4
IN_SELF_PAIRS_IMP_EE_EMPTY
IN_SELF_PAIRS_IMP_FST_EQ_SND_FORALL
IN_SET_IMP_IN_CONVEX_HULL_SET
IN_SET_OF_EDGE
IN_SPAN_DELETE
IN_SPAN_IMAGE_BASIS
IN_SPAN_INSERT
IN_SYM_0
IN_TRANS
IN_VO2_EQ
IN_VORONOI_LIST_IMP_IN_BIS
IN_VO_EQ
IN_V_IMP_AZIM_LESS_PI
IN_V_IMP_AZIM_LESS_PI_ALT
IN_WEDGE_IMP_AZIM_LE
IPVICGW
IPVICGW_C33
IPVICGW_C43_C44
IPVICGW_C5_QX_ALONG_NOT_SMALL
IQCPCGW
ISOMETRY_LINEAR
ISOMETRY_SPHERE_EXTEND
ISOMETRY_SUBSPACES
ISOMETRY_UNIV_SUBSPACE
ISOMETRY_UNIV_SUPERSET_SUBSPACE
ISOMETRY_UNIV_UNIV
ISOMORPHISMS_UNIV_UNIV
ISOMORPHISM_COMPONENT_IMAGE
ISOMORPHISM_EXPAND
ISOMORPHISM_FAN_LIST
ISOMORPHISM_IMP_ISO
ISOMORPHISM_INVERSE
ISO_FACE_INJ
ISO_IMP_ISOMORPHISM
ISO_NODE_INJ
ISRTTNZ
IS_EAR_IS_SCS
IS_EAR_V25_EQ_EAR_SY
IS_SCS_NOT_COLLINEAR_BBs_CASE_3
IS_SCS_NOT_COLLINEAR_BBs_CASE_LE_3
IS_SCS_NOT_COLLINEAR_BBs_CASE_LE_PRIME_3
IS_SCS_POINT_IN_BBS_IS_NOT_0_3
IS_SCS_POINT_IN_BBS_IS_NOT_0_LE_3
IS_SCS_STABLE_SYSTEM
IS_SCS_TRI_STABLE_SYSTEM
IS_SY
ITER1
ITER12
ITER_AZIM_CYCLE_EQ_ITER_SIGMA
ITER_CARD_MINUS1_EQ_IVS_RN1
ITER_CARD_W_IDENTIFICATION
ITER_COMM_RESTRICTED
ITER_CROSS_SAME_DIRECTION
ITER_CYCLIC_ORBIT
ITER_IN_AFF_GT_2_1
ITER_IVS_RHO_IDD
ITER_N_I
ITER_RHO_IVS_IDD
ITER_vv_rho_node1
ITLIST2_EQ_SUM
ITLIST_DISJ_APPEND
IUNBUIG
IVFICRK
IVFICRK_real3
IVS_AZIM_AS_SIGMA_FAN
IVS_AZIM_CYCLE_SING
IVS_AZIM_CYCLE_SYM_0
IVS_AZIM_CYCLE_TWO_POINT_SET
IVS_AZIM_CYCLE_TWO_POINT_SET_ALT
IVS_AZIM_EMPTY_IDE
IVS_AZIM_EQ_INVERSE_SIGMA_FAN
IVS_AZIM_EQ_INVERSE_SIGMA_FAN2
IVS_AZIM_PROPERTIES
IVS_RHO_IDD
IVS_RHO_NODE1_DETE
IVS_RHO_NODE1_IN_V
IVS_RHO_NODE_DIFF_ID
IVS_RHO_NODE_IN_EDGE
IVS_RHO_NODE_V_IN_FF
IVS_RNODE_IN_AFF_V
IVT_delta_x
IVT_delta_x_3
IVT_delta_x_5
IVT_delta_x_6
IVT_delta_x_full
IVT_delta_y_full
IVT_edge2_flatD_x1
IXPOTPA_MERGED
I_BIJ
I_IMP
I_LT_J_LT_3_EXPLICIT
I_LT_J_LT_4_EXPLICIT
I_LT_J_LT_5_EXPLICIT
I_SY
I_TS
i_IN_ORBITS_FAN
i_c1
i_fan
i_half
i_mhalf
i_mone
i_one_twelfth
i_th0
iabs
id3
id4
id4a
id4b
id5
id_enf_fan
id_power_enf_fan
idempotent
identify_inj_contour
identity_face_in_face_set
identity_node_in_face_set
identity_scale
idz
if_azims_fan
if_azims_works_fan
image_power_map_points
imp_eq
imp_inv_norm_not_zero_fan
imp_le
imp_lt
imp_norm_ge_zero_fan
imp_norm_gl_zero_fan
imp_norm_not_zero_fan
imp_nz
import_le
in_VC
in_aff_2_2_fan
in_aff_ge_0_2
in_aff_ge_0_2_imp_dot_pos
in_aff_ge_cases_lemma
in_aff_ge_dist_lemma
in_aff_ge_dist_lower_bound
in_aff_ge_fan
in_aff_gt_1_2
in_aff_gt_eq_azim
in_affine_hull_lemma
in_ball_annulus
in_ccube_floor
in_d1
in_direction_fan
in_inv
in_list
in_orb
in_orbit_lemma
in_orbit_map1
in_preimage
in_segment_imp_in_aff_ge_0_2
in_set_of_orbits
in_topological_component_yfan_is_connected
incident_edges
incr_nth
ind
independent
independent_run_edges_fan
index
index_representation
ineq
ineq'
ineq6_of_ineq1
ineq6_of_ineq5
ineq_5691615370_asym
ineq_APPEND
ineq_CONJ
ineq_MP
ineq_T
ineq_af
ineq_approxA_ztg4
ineq_branch_2hmin
ineq_branch_edge
ineq_branch_edge_strict
ineq_constant
ineq_critical_edge
ineq_critical_edge2
ineq_critical_edge3
ineq_critical_edge4
ineq_expand6
ineq_expand9
ineq_lemma_b
ineq_lm5_3_step3
ineq_lm5_3_step4
ineq_monotone
ineq_pathL_pathR
ineq_square2
ineq_square2_9
ineq_sym_s2_aab
ineq_sym_s2_abb
ineq_sym_s3
ineq_th
inequaility2_fan
inequaility2_not0_fan
inequality1_fan
inequality1_not0_fan
inequality3_aim_in_convex_fan
inequality4_aim_in_convex_fan
inf_ex
inf_pos
inf_pos_y
infi_lemma2
infnorm
initial_sublist_cons
inj_cube
inj_iterate_lemma
inj_iterate_segment
inj_map1
inj_map3
inj_map_to_voronoi
inj_orbit
inj_orbit_imp_inj_face_contour
inj_orbit_imp_inj_node_contour
inj_orbit_step
inj_path
injective
injective_azim_coplanar
insert_v
int_ball
int_ball_card_eq
int_ball_card_eq_ccube
int_ball_subset
int_ball_subset_CROSS
int_interval
integer_point
inter_aff_ge_3_1_is_aff_ge_1_3
inter_aff_ge_3_1_is_aff_ge_2_2
inter_aff_gt_3_1_is_aff_gt_1_3
inter_aff_gt_3_1_is_aff_gt_2_2
inter_is_empty
inter_radial
interior_angle
interior_angle1
interior_angle1_azim
interior_angle1_azim_scs
interior_contour
interior_fan
interior_point
interior_pos
interp
intersection_point_exists
interval_arith
interval_arith_abs_le
interval_eps
interval_fan
interval_not_zero
interval_pos
interval_upper_lowerbound
into_domain1_e_fan
into_domain1_f1_fan
into_domain1_n_fan
into_domain1_power_efn_fan
into_domain_e_fan
into_domain_efn_fan
into_domain_f1_fan
into_domain_n_fan
into_domain_power_efn_fan
inv1_diag
inv1_diag1
inv2_eq_lemma
inv_add_mod
inv_diag
inv_diag1
inv_iso
inv_partial_lemma'
inv_second_lemma'
inv_twopow
invariant_cross_dotr_esilon_3piont
invariant_crossr_dot_esilon_3piont
invariant_rcross_dot_esilon_3piont
inverse1_sigma_fan
inverse1_sigma_fan_FANADD
inverse1_sigma_fan_FANADD1
inverse1_sigma_fan_FANADD2
inverse1_sigma_fan_FANADD3
inverse1_sigma_fan_FANADD4
inverse2_hypermap_maps
inverse_element_lemma
inverse_element_via_order
inverse_function
inverse_hypermap_maps
inverse_power_function
inverse_relation
inverse_sigma_fan
inverse_sigma_fan_alt
invert_den_eq
invert_den_le
invert_den_lt
invertible
involutive
iota
ipows2
ipowsc2
isSome
is_Moebius_contour
is_circular_clf
is_contour
is_contour_loop
is_cyclic_permutation
is_deformation_clf
is_disjoint
is_ear_3603097872
is_ear_scs3
is_ear_v39
is_edge_degenerate
is_edge_merge
is_edge_nondegenerate
is_edge_split
is_face_contour
is_face_degenerate
is_face_loop
is_face_merge
is_face_nondegenerate
is_face_split
is_flat
is_generic_clf
is_glueing
is_in_canon_darts
is_in_component
is_inj_contour
is_inj_list
is_loop
is_lunar_clf
is_marked
is_no_double_joins
is_no_double_joints
is_node_degenerate
is_node_going
is_node_merge
is_node_nondegenerate
is_node_split
is_normal
is_path
is_restricted
is_scs_3I1
is_scs_3M1
is_scs_3T1
is_scs_3T2
is_scs_3T3
is_scs_3T4
is_scs_3T5
is_scs_3T6
is_scs_3T7
is_scs_4I1
is_scs_4I2
is_scs_4I3
is_scs_4M1
is_scs_4M2
is_scs_4M3
is_scs_4M4
is_scs_4M5
is_scs_4M6
is_scs_4M7
is_scs_4M8
is_scs_4T1
is_scs_4T2
is_scs_4T3
is_scs_4T4
is_scs_4T5
is_scs_5I1
is_scs_5I2
is_scs_5I3
is_scs_5M1
is_scs_5M2
is_scs_5T1
is_scs_6I1
is_scs_6M1
is_scs_6T1
is_scs_adj
is_scs_ear_3603097872
is_scs_examples
is_scs_funlist
is_scs_funlist_basic
is_scs_k_le_3
is_scs_scs3
is_scs_slice_v39
is_scs_v39
is_solution
is_split_condition
is_splitting_component
isabelle_graph_class_axiom3
iso
iso_card_eq
iso_dart3_trans
iso_dart4_trans
iso_dartX_trans
iso_dart_in
iso_dart_trans
iso_edge_pairs_trans
iso_face3_trans
iso_face4_trans
iso_face5_trans
iso_face6_trans
iso_face_card
iso_face_trans
iso_node_trans
iso_reflect
iso_sym
iso_trans
isolated_dart
isolated_pai
isolated_pair
isolated_qua
isomorphism
iter
iter_sigma_fan_in_set_of_edge
iter_spec
iterate_map_valuation
iterate_map_valuation2
iterate_orbit
iteri
ivs_azim_cycle
ivs_azim_cycle_elim
ivs_rho_node1