HOL html

Files Index

Theorems Index

F (theorems)

FACE3_LIST_ALL
FACE4_LIST_ALL
FACE5_LIST_ALL
FACE6_LIST_ALL
FACES_HYPERMAP_OF_LIST_ALL
FACET_AFF_DIM_2
FACET_FINITE
FACET_INTER_DISJOINT
FACET_OF_POLYHEDRON_EXPLICIT_ALT
FACET_OF_POLYHEDRON_EXPLICIT_BIS
FACET_OF_SEGMENT
FACET_RELEVANT
FACET_SOL_NN
FACET_SUBSET_CLOSURE_FCHANGED
FACE_ALL_SYM_0
FACE_CYCLE_CARD
FACE_DUAL_SYM_0
FACE_FAN_NOT_EMPTY
FACE_FINITE
FACE_HYPERMAP_OF_LIST_EXPLICIT
FACE_HYP_FAN_SY
FACE_HYP_FAN_SY1
FACE_LAST_POINT
FACE_MAP_ADD_SET2_EQ
FACE_MAP_AT_TURNING_DART
FACE_MAP_AT_TURNING_DART1
FACE_MAP_SLICING_HYP_TRANS_POINT
FACE_NODE_EDGE_ORBIT_INVERSE
FACE_NOT_EMPTY
FACE_OF_LIST
FACE_OF_SIZE_2
FACE_SET_EQ_LIST
FACE_SUBSET_DART1_OF_FAN
FACE_SUBSET_DARTS
FACE_SUBSET_DART_OF_FAN
FACE_SUM_lemma
FACE_SYM_0
FACTOR_OF_QUADRARTIC
FAFKVLR
FAFKVLR_ALT
FALSE_ALL
FAN
FAN1_LINEAR_IMAGE_EQ
FAN1_TRANSLATION_EQ
FAN2_LINEAR_IMAGE_EQ
FAN2_TRANSLATION_EQ
FAN3_LINEAR_IMAGE_EQ
FAN3_TRANSLATION_EQ
FAN4_LINEAR_IMAGE_EQ
FAN4_TRANSLATION_EQ
FAN5_LINEAR_IMAGE_EQ
FAN5_TRANSLATION_EQ
FAN6_LINEAR_IMAGE_EQ
FAN6_TRANSLATION_EQ
FAN7_AFF_GT_CONDITION
FAN7_LINEAR_IMAGE_EQ
FAN7_SIMPLE
FAN7_SMALL_DEFORMATION
FAN7_TRANSLATION_EQ
FAN80_FANADD
FANADD_CONFORMING
FANO
FANO_OF_FAN
FAN_AFF2_INTER_CONV0_IMP_NO_IN_AF
FAN_AFF_GT_CONDITION
FAN_DARTS_OF_IN_D
FAN_DART_DARTS
FAN_ECONOMIZED
FAN_ECONOMIZED_SIMPLE
FAN_EDGE_EL_V
FAN_EDGE_SUBSET_V
FAN_E_SUB_V
FAN_FACE_GT1_IMAGE_EE_OF_HYP
FAN_FACE_IMP_IVS_F_IN_F
FAN_FST_EQ_SND_SUPPER_EQ
FAN_IMP_BIJ_V_NODE_OF_HYP
FAN_IMP_DIFF
FAN_IMP_EE_EQ_SET_OF_EDGE
FAN_IMP_FACE_MAP_PERMUTES_DARTS
FAN_IMP_FIMITE_DARTS
FAN_IMP_FINITE_DARTS
FAN_IMP_FINITE_EE
FAN_IMP_IN_DARTS_IFF_FF_TOO
FAN_IMP_IN_SELF_PAIRS_IFF_FF_OF_HYP
FAN_IMP_NN_OF_HYP_PERMUTES_DARTS
FAN_IMP_NOT_EMPTY_DARTS
FAN_IMP_NOT_IN_AFF_GE
FAN_IMP_V_DIFF
FAN_INTERSECTION_PRO_EXPRESS
FAN_IN_AFF_GE_IMP_EQ
FAN_IN_DARTS_FST_EQ_SND_SELF_PAIRS
FAN_IN_E_DIFF
FAN_IN_SEFL_PAIRS_IMP_PROGORIOUS_DEGENERATE
FAN_IN_SET_OF_EDGE
FAN_LINEAR_IMAGE_EQ
FAN_NODE_EQ_lemma
FAN_PAIR_FIXED_POINT
FAN_PERIMETER
FAN_PERIMETER_INVARIANT
FAN_PERIMETER_INVARIANT_CARD_V
FAN_SINGLETON_V_DARTS
FAN_SUB_NOT_EQ_COLL_IN_CONV0
FAN_SYM_0
FAN_TRANSLATION_EQ
FAN_V_TWO_ELMS_IN_E_DARTS2
FATUGPD_quasi
FCC_COMPATABILITY_FUNC
FCHANGED_AFFINE
FCHANGED_EQ_YFAN
FCHANGED_IN_COMPONENT
FCHANGED_LINEAR_INVARIANT
FCHANGED_MEASURABLE
FCHANGED_ONE_TO_ONE
FCHANGED_OPEN
FCHANGED_RADIAL
FCHANGED_RADIAL_ALT
FCHANGED_SUBSET_YFAN
FCHKUGT
FEBRUARY_13_09
FEKTYIY
FF
FF_DISJOINT_ITS_IMAGE_CARD_EQ
FF_IMAGE_EE_OF_HYP_EQ_E_PRIME
FF_OF_HYP_EQ
FF_OF_HYP_EQ1
FF_OF_HYP_HAS_ORDERS
FF_OF_HYP_ITER_VV
FF_OF_HYP_NOT_EQ_ID
FF_OF_HYP_POWER_EQ_ID
FGNMPAV
FHFMKIY
FILTER_A_EMPTY
FILTER_NODE_EMPTY
FIND_FACE
FIND_FACE_EMPTY
FIND_FACE_F_LIST
FIND_FACE_LEMMA_EXPLICIT
FIND_PAIR_LIST_UNIQUE
FININTE_GFUN
FINITENESS_OF_K_FIRST_ELMS
FINITE_AND_LOOP_IMP_BIJ_S_IM_S
FINITE_BIJ
FINITE_BIJ2
FINITE_BOUNDED_FUNCTIONS
FINITE_CARD1_IMP_SINGLETON
FINITE_COUNTABLE
FINITE_DART_OF_FAN
FINITE_EDGE
FINITE_EDGE_X2
FINITE_FACE_FAN
FINITE_F_SY
FINITE_HAS_SIZE_LEMMA
FINITE_HYPERMAP_COMPONENTS
FINITE_HYPERMAP_ORBITS
FINITE_IMAGE_F_SY
FINITE_IMAGE_INJ
FINITE_IMP_BOUNDED_FAN
FINITE_IMP_CLOSED_FAN
FINITE_IMP_COMPACT_FAN
FINITE_INDEX_NUMSEG_SPECIAL
FINITE_INITIAL_SEG2
FINITE_INJ
FINITE_J1_SY
FINITE_J1_TS
FINITE_J_SY
FINITE_LIST_KY_LEMMA_2
FINITE_LIST_klemma
FINITE_MAX_EXISTS
FINITE_MCELL_SET_LEMMA
FINITE_MCELL_SET_LEMMA_2
FINITE_MCELL_SET_lemma1
FINITE_NODE_FAN
FINITE_OF_N_FIRST_ELMS
FINITE_ORBITS_SIGMA_FAN
FINITE_ORBIT_MAP
FINITE_ORBIT_MAP_EXPLICIT
FINITE_ORBIT_MAP_INVERSE
FINITE_PERMUTE_3
FINITE_PERMUTE_4
FINITE_PRODUCT_IMAGE
FINITE_SCS_M
FINITE_SERIES
FINITE_SET_LIST_LEMMA
FINITE_SET_PRODUCT_KY_LEMMA
FINITE_SET_STR
FINITE_SEUBSET_OF_NATURAL
FINITE_SING
FINITE_SINGLETON
FINITE_STDBASIS
FINITE_SYM_0
FINITE_TOPOLOGICAL_COMPONENT_YFAN
FINITE_TWO_ELEMENTS
FINITE_VX
FINITE_critical_edgeX
FINITE_edgeX
FINTE_OF_N_FIRST_ELMS2
FIN_LOOP_IMP_BIJ_ITSELF
FIRST_AAUHTVE
FIRST_AAUHTVE2
FIRST_AZIM_CYCLE_EQ_RHO_NODE
FIRST_DERIVATIVE_TEST_TAUM
FIRST_DERIV_POS_OPEN_COMPOSE
FIRST_EQ0_LAST_LT_PI
FIRST_IN_AFF
FIRST_NOV22
FIRST_POINT_IN_AFF3
FLATTEN
FLATTEN_A_EMPTY
FLATTEN_CLAUSES
FLATTEN_FILTER_EMPTY
FLOAT_0
FLOAT_ABS
FLOAT_ADD
FLOAT_ADD_EQ
FLOAT_ADD_FF
FLOAT_ADD_FF_hi
FLOAT_ADD_FF_lo
FLOAT_ADD_FT_F_hi
FLOAT_ADD_FT_F_lo
FLOAT_ADD_FT_T_hi
FLOAT_ADD_FT_T_lo
FLOAT_ADD_NN
FLOAT_ADD_NNv2
FLOAT_ADD_NP
FLOAT_ADD_PN
FLOAT_ADD_PP
FLOAT_ADD_PPv2
FLOAT_ADD_TT
FLOAT_ADD_TT_hi
FLOAT_ADD_TT_lo
FLOAT_ATN_LO_HI
FLOAT_DIV_0x_hi
FLOAT_DIV_0x_lo
FLOAT_DIV_FF
FLOAT_DIV_FF_hi
FLOAT_DIV_FF_lo
FLOAT_DIV_FT_hi
FLOAT_DIV_FT_lo
FLOAT_DIV_TF_hi
FLOAT_DIV_TF_lo
FLOAT_DIV_TT_hi
FLOAT_DIV_TT_lo
FLOAT_EQ
FLOAT_EQ_0
FLOAT_F_GE_0
FLOAT_F_LT
FLOAT_F_LT_0
FLOAT_F_POS
FLOAT_IABS_FF
FLOAT_IABS_TT
FLOAT_INTERVAL_ACS
FLOAT_INTERVAL_DIV_FF_FF
FLOAT_INTERVAL_DIV_FF_TT
FLOAT_INTERVAL_DIV_FT_xx
FLOAT_INTERVAL_DIV_TF_FF
FLOAT_INTERVAL_DIV_TF_TT
FLOAT_INTERVAL_DIV_TT_FF
FLOAT_INTERVAL_DIV_TT_TT
FLOAT_INTERVAL_FT_IMP_0
FLOAT_INTERVAL_GT0
FLOAT_INTERVAL_INV
FLOAT_INTERVAL_LT
FLOAT_INTERVAL_NEG
FLOAT_INTERVAL_SQRT
FLOAT_LE
FLOAT_LE_FF
FLOAT_LE_FT
FLOAT_LE_TF
FLOAT_LE_TT
FLOAT_LT
FLOAT_LT_FF
FLOAT_LT_FT
FLOAT_LT_TT
FLOAT_MUL
FLOAT_MUL_FF
FLOAT_MUL_FT
FLOAT_MUL_TF
FLOAT_MUL_TT
FLOAT_NEG
FLOAT_POS
FLOAT_POW
FLOAT_PRE_EXP
FLOAT_SQRT_EVEN_hi
FLOAT_SQRT_EVEN_lo
FLOAT_SUB
FLOAT_T_GT_0
FLOAT_T_LE_0
FLOAT_T_NEG
FLOAT_ZERO
FLOOR_EQ
FLVNSME
FM_DEMOD
FORALL_1
FORALL_2
FORALL_3
FORALL_BIJ_SQUARE
FORALL_DIMINDEX_1
FORALL_DOT_EQ_0
FORALL_DROP
FORALL_DROP_FUN
FORALL_LIFT
FORALL_LIFT_FUN
FORALL_REAL_ONE
FORALL_TRIPLED_THM
FORALL_VECTOR_1
FORALL_VECTOR_2
FORALL_VECTOR_3
FOR_AFF_GT_NOT_INTERSECTION
FOR_LEMMA19
FOUR_POINTS
FRONTIER_BALL_FAN
FRONTIER_CBALL_FAN
FRONTIER_CLOSED_FAN
FRONTIER_CLOSURES_FAN
FRONTIER_STRADDLE_FAN
FRONTIER_SUBSET_CLOSED_FAN
FRONTIER_SUBSET_COMPACT_FAN
FRUSTT_RCONE_GE
FRUSTT_WEDGE_RCONE_GE
FSQKWKK
FSTCART_ADD
FSTCART_CMUL
FSTCART_NEG
FSTCART_SUB
FSTCART_VEC
FSTCART_VSUM
FST_BIJ
FST_EQ_IF_SAME_SND
FST_LST_IN_WEDGE_GE
FST_NODE_HYPERMAP_OF_FAN
FST_NODE_lemma
FST_N_LIST_EXT_POWER
FST_SND_EQ_PAIR_SYM_0
FST_SND_NEG_PAIR_SYM_0
FST_SND_PAIR_SYM_0
FST_SND_X_IN_EE_E_PRIME
FUEIMOV_3
FUEIMOV_4
FUEIMOV_K
FULLY_SURROUNDED
FULLY_SURROUNDED_IMP_CARD_FACE_GE_3
FULLY_SURROUNDED_IMP_CARD_NODE_EQ_SUM_NODE_TYPE
FULLY_SURROUNDED_NODE_DECOMPOSITION
FULLY_SURROUND_IS_NON_ISOLATED_FAN2
FULL_RANK_INJECTIVE
FULL_RANK_SURJECTIVE
FUN
FUNLIST_EXPLICIT
FUNOUYH_SLICE
FUN_AFFINE_KLEMMA
FUN_COMMUTATIVE
FUN_V3_DEFOR
FUN_V3_DEFOR_V5
FUN_WW_DEFOR
FUZBZGI_0
FUZBZGI_1
FX_IN_S_IMP_F_POWER_TOO
FX_IN_S_IMP_ORBIT_SUBSET
FYSSVEV
FZIOTEF
FZIOTEF_REFL
FZIOTEF_TRANS
FZIOTEF_UNION
F_DEFORMATION_V3_DEFOR
F_DEFORMATION_V3_DEFOR_V5
F_DEFORMATION_WW_DEFOR
F_DEMOD
F_FAN_PAIR_EXT
F_FAN_PAIR_EXT_PERMUTES_DART1_OF_FAN
F_FAN_PAIR_EXT_PERMUTES_DART_OF_FAN
F_HAS_NO_FIXED_POINTS_IN_D1
F_HAS_ORDERS_IMP_FINITE_ORBIT
F_INVERSE_F
F_LIST_EXT_INVERSE
F_LIST_EXT_INVERSE_WORKS
F_LIST_EXT_ORBIT
F_LIST_EXT_PERMUTES_DARTS
F_LIST_EXT_TABLE
F_LIST_INVERSE
F_PRIME_EQ_F_vv
F_SUC_PRE
F_SY
F_SY_COVER_EQ
F_SY_COVER_INTER
F_SY_EQ_FACE
F_SY_EQ_FACE1
F_SY_INTER_IMAGE_NN_EMPTY
f10_in_d1_fanadd
f1_fan
f1_fan_of_f10_eq_f20
f1_fan_of_f20_eq_f30
f1_fan_of_f30_eq_f10
f1_fan_permutes
f1_fan_permutes_prime
f1_fan_power_in_face
f1_fan_power_in_face_imp_in_face
f2_EQ_F30_FANADD
f_ex
f_fan
f_fan_no_fix_point
f_fan_pair
f_fan_pair_ext
f_hyp_of_fan
f_list
f_list_ext
f_list_ext_table
f_of_hyp
f_sy
f_ts
fa4
fa5
face
face_collection
face_contour
face_cyclic_map_lemma
face_datum
face_deform
face_degenerate_walkup_edge_map
face_degenerate_walkup_face_map
face_loop
face_loop_lemma
face_loop_rep
face_map
face_map_and_darts
face_map_face_walkup
face_map_injective
face_map_inverse_representation
face_map_node_walkup
face_map_of_fan
face_map_on_margin
face_map_restrict
face_map_walkup
face_of_node
face_path
face_quotient_lemma
face_refl
face_set
face_set_k
face_set_of_fan
face_set_of_node
face_slice
face_step_contour
face_subset_dart_fan
face_walkup
faces_of_list
facet_3_facets
facet_arg_lt_pi
facet_rep_a_uniq
facet_rep_def
facet_rep_in_facet
facet_rep_in_poly
facet_rep_not_in_facet
facet_rep_nz
facet_rep_refl
facet_rep_spec
facet_rep_uniq
facet_rep_uniq_c
factor345_hexall_x
factorial_lemma
fan
fan1
fan11
fan1_lemma
fan2
fan21
fan2_lemma
fan3
fan31
fan3_lemma
fan4
fan41
fan5
fan51
fan6
fan7
fan7_2
fan7_3
fan7_4_0
fan7_4_1
fan7_4_1_cases
fan7_4_1_one_case
fan7_4_2
fan80
fan81
fan_card
fan_datum
fan_intersection
fan_list_iso
fan_list_nodes_iso
fan_nonparallel
fan_of_FAN
fan_of_polyhedron
fan_origin
fan_run1_in_small_is_fan
fan_run1_in_small_not0_is_fan
fan_run_in_small11_not0_is_fan
fan_run_in_small1_is_fan
fan_run_in_small1_not0_is_fan
fan_run_in_small21_is_fan
fan_run_in_small2_is_fan
fan_run_in_small2_not0_is_fan
fan_run_in_small3_is_fan
fan_run_in_small3_not0_is_fan
fan_run_in_small_is_fan
fan_run_in_small_is_not_meet_xfan
fan_run_in_small_is_subset_yfan
fan_run_in_small_not0_is_fan
fat_lemma1
fc_ex
fcc_compatible
fcc_ineq
fchanged
fd
fd_ex
fdodec
ff_FUN_COMMUTATIVE_SYM_0
ff_POWER_COMMUTATIVE_SYM_0
ff_of_hyp
ff_of_hyp2
ff_of_hyp3
ff_of_hyp_elim
filter
filter_FILTER
filter_nodes_empty
fin_lem
find
find_dia
find_diagonal
find_face
find_list
find_pair_list
fini_lemma
fini_lemma1
finish_avoids1_fan
finish_avoids_fan
finite_cross_int_interval
finite_d1_fan
finite_d20_fan
finite_d_fan
finite_int_ball
finite_int_interval
finite_nfan
finite_num_func_attain_max
finite_orbits_lemma
finite_order
finite_set_of_ccube
finite_set_of_cube
finite_set_packing_in_ball
finite_set_voronoi_center_in_ball
finite_voronoi2
first_glue_evaluation
first_join_evaluation
first_unique_choice
fix
fix_point_sigma_fan
fixed_point_lemma
fl_sy
flag
flat_term
flat_term2_126_x
flat_term2_126_x_eval
flat_term2_135_x
flat_term2_135_x_eval
flat_term2_234_x
flat_term_126_x
flat_term_135_x
flat_term_2
flat_term_2h0
flat_term_neg
flat_term_sol0
flat_term_x
flatten
flatten_empty
float
floor_ineq
fmap_permute
fmap_via_choice
fn_fun
fn_sub246
fn_sub345
foldl
foldr
four6
fourier
from_tail
frontier_fan
frotier_closures_fan
frustt
frustum
fully_surrounded
fully_surrounded_imp_aff_gt_3_1_of_dart_eq_fan
fully_surrounded_imp_aff_gt_3_1_of_edge_eq_fan
fully_surrounded_is_non_isolated_fan
func
func1
functional1_flat_term_x
functional1_lfun
functional1_rho
functional_acs_sqrt_x1_d4
functional_acs_sqrt_x2_d4
functional_arclength_126
functional_arclength_234
functional_arclength_x1
functional_arclength_x2
functional_arclength_x_123
functional_asn797k
functional_asnFnhk
functional_delta4_squared_x
functional_delta_126_x
functional_delta_135_x
functional_delta_234_x
functional_delta_pent_x
functional_delta_sub1_x
functional_delta_x1
functional_delta_x_126_s2
functional_delta_x_135_s2
functional_dih2_x
functional_dih2_x_126_s2
functional_dih2_x_135_s2
functional_dih3_x
functional_dih3_x_126_s2
functional_dih3_x_135_s2
functional_dih3_x_div_sqrtdelta_posbranch
functional_dih4_x
functional_dih4_x_126_s2
functional_dih4_x_135_s2
functional_dih5_x
functional_dih5_x_126_s2
functional_dih5_x_135_s2
functional_dih5_x_div_sqrtdelta_posbranch
functional_dih6_x
functional_dih6_x_126_s2
functional_dih6_x_135_s2
functional_dih_x_126_s2
functional_dih_x_135_s2
functional_dih_x_div_sqrtdelta_posbranch
functional_dnum1
functional_edge2_126_x
functional_edge2_135_x
functional_edge2_234_x
functional_edge_flat2_x
functional_eta2_126
functional_eta2_135
functional_eta2_456
functional_eulerA_x
functional_euler_1flat_x
functional_euler_2flat_x
functional_euler_3flat_x
functional_gamma3f_x_v_lfun
functional_gchi1_x
functional_gchi2_x
functional_gchi3_x
functional_gchi4_x
functional_gchi5_x
functional_gchi6_x
functional_halfbump_x1
functional_halfbump_x4
functional_ldih2_x
functional_ldih2_x_126_n
functional_ldih2_x_126_s2
functional_ldih3_x
functional_ldih3_x_135_n
functional_ldih3_x_135_s2
functional_ldih5_x_135_n
functional_ldih5_x_135_s2
functional_ldih6_x
functional_ldih6_x_126_n
functional_ldih6_x_126_s2
functional_ldih_x
functional_ldih_x_126_n
functional_ldih_x_126_s2
functional_ldih_x_135_n
functional_ldih_x_135_s2
functional_ldih_x_div_sqrtdelta_posbranch
functional_ldih_x_n
functional_lfun_y1
functional_mud_126_x
functional_mud_135_x
functional_mud_234_x
functional_norm2hh_x
functional_proj_x1
functional_proj_x2
functional_proj_x3
functional_proj_x4
functional_proj_x5
functional_proj_x6
functional_proj_y1
functional_proj_y2
functional_proj_y3
functional_proj_y4
functional_proj_y5
functional_proj_y6
functional_rhazim2_x
functional_rhazim2_x_div_sqrt_delta_posbranch
functional_rhazim3_x
functional_rhazim3_x_div_sqrt_delta_posbranch
functional_rhazim_x
functional_rhazim_x_div_sqrt_delta_posbranch
functional_rotate2
functional_rotate3
functional_rotate4
functional_rotate5
functional_rotate6
functional_sol156_euler_x_div_sqrtdelta
functional_sol246_euler_x_div_sqrtdelta
functional_sol345_euler_x_div_sqrtdelta
functional_sol_euler_x_divsqrtdelta
functional_tau_residual
functional_taum_1flat_x
functional_taum_2flat_x
functional_taum_3flat_x
functional_taum_sub1_x
functional_taum_sub246_x
functional_taum_sub345_x
functional_taum_x
functional_taum_x1
functional_taum_x1_x2
functional_taum_x2
functional_ups_126
functional_vol3_x_135_s2
functional_vol3_x_sqrt
functional_vol3f_x_lfun
functional_vol3f_x_sqrt2_lmplus
functional_vol_x
functional_x1_delta_x
funlistA_diag
funlistA_empty
funlistA_sym
funlistA_v39
funlist_diag
funlist_kik
funlist_sym
funlist_v39