HOL html

Files Index

Theorems Index

F (theorems)

FACES_OF_LINEAR_IMAGE
FACES_OF_SIMPLEX
FACES_OF_TRANSLATION
FACETS_OF_POLYHEDRON_EXPLICIT_DISTINCT
FACET_OF_CONVEX_HULL_AFFINE_INDEPENDENT
FACET_OF_CONVEX_HULL_AFFINE_INDEPENDENT_ALT
FACET_OF_EMPTY
FACET_OF_HALFSPACE_GE
FACET_OF_HALFSPACE_LE
FACET_OF_IMP_FACE_OF
FACET_OF_IMP_PROPER
FACET_OF_IMP_SUBSET
FACET_OF_LINEAR_IMAGE
FACET_OF_POLYHEDRON
FACET_OF_POLYHEDRON_EXPLICIT
FACET_OF_REFL
FACET_OF_TRANSLATION_EQ
FACE_OF_AFFINE_EQ
FACE_OF_AFFINE_TRIVIAL
FACE_OF_AFF_DIM_LT
FACE_OF_CONIC
FACE_OF_CONVEX_HULLS
FACE_OF_CONVEX_HULL_AFFINE_INDEPENDENT
FACE_OF_CONVEX_HULL_INSERT
FACE_OF_CONVEX_HULL_INSERT_EQ
FACE_OF_CONVEX_HULL_SUBSET
FACE_OF_DISJOINT_INTERIOR
FACE_OF_DISJOINT_RELATIVE_INTERIOR
FACE_OF_EMPTY
FACE_OF_EQ
FACE_OF_FACE
FACE_OF_HALFSPACE_GE
FACE_OF_HALFSPACE_LE
FACE_OF_IMP_CLOSED
FACE_OF_IMP_COMPACT
FACE_OF_IMP_CONVEX
FACE_OF_IMP_SUBSET
FACE_OF_INTER
FACE_OF_INTERS
FACE_OF_INTER_INTER
FACE_OF_INTER_SUBFACE
FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE
FACE_OF_INTER_SUPPORTING_HYPERPLANE_GE_STRONG
FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE
FACE_OF_INTER_SUPPORTING_HYPERPLANE_LE_STRONG
FACE_OF_LINEAR_IMAGE
FACE_OF_PCROSS
FACE_OF_PCROSS_DECOMP
FACE_OF_PCROSS_EQ
FACE_OF_POLYHEDRON
FACE_OF_POLYHEDRON_EXPLICIT
FACE_OF_POLYHEDRON_POLYHEDRON
FACE_OF_POLYHEDRON_SUBSET_EXPLICIT
FACE_OF_POLYHEDRON_SUBSET_FACET
FACE_OF_POLYTOPE_POLYTOPE
FACE_OF_REFL
FACE_OF_REFL_EQ
FACE_OF_SIMPLEX_SUBSET
FACE_OF_SING
FACE_OF_SLICE
FACE_OF_STILLCONVEX
FACE_OF_SUBSET
FACE_OF_SUBSET_RELATIVE_BOUNDARY
FACE_OF_SUBSET_RELATIVE_FRONTIER
FACE_OF_TRANS
FACE_OF_TRANSLATION_EQ
FACT
FACTORIZATION_INDEX
FACTOR_1X4_LEMMA
FACT_DIVIDES
FACT_DIV_LCANCELS
FACT_DIV_MULT
FACT_DIV_RCANCELS
FACT_DIV_SIMP
FACT_EXPAND_PSI
FACT_LE
FACT_LE_REFL
FACT_LT
FACT_MONO
FACT_NPRODUCT
FACT_NZ
FACT_PRODUCT
FACT_PRODUCT_ALT
FACT_PSI_BOUND_2_3
FACT_PSI_BOUND_EVEN
FACT_PSI_BOUND_ODD
FALSE
FALSE_def
FARKAS_LEMMA
FARKAS_LEMMA_ALT
FASHODA
FASHODA_INTERLACE
FASHODA_UNIT
FASHODA_UNIT_PATH
FCONS
FCONS_UNDO
FCT1_WEAK
FC_FINITE_BOUND
FC_FINITE_BOUND_LEMMA
FEJER_KERNEL
FEJER_KERNEL_CONTINUOUS
FEJER_KERNEL_CONTINUOUS_STRONG
FEJER_KERNEL_POS_LE
FERMAT_LITTLE
FERMAT_LITTLE_COPRIME
FERMAT_LITTLE_PRIME
FERMAT_LITTLE_VARIANT
FEUERBACH
FILTER
FILTER_APPEND
FILTER_DELETE1
FILTER_MAP
FINE_DIVISION_EXISTS
FINE_INTER
FINE_INTERS
FINE_MIN
FINE_SUBSET
FINE_UNION
FINE_UNIONS
FINITELY_GENERATED_CONIC_POLYHEDRON
FINITE_ATMOST
FINITE_BALL
FINITE_BIJ
FINITE_BIJ2
FINITE_BITSET
FINITE_BOOL
FINITE_BOUNDED_FUNCTIONS
FINITE_BOUNDED_INTEGER_POINTS
FINITE_CARD_COMPLEX_ROOTS_UNITY
FINITE_CARD_COMPLEX_ROOTS_UNITY_EXPLICIT
FINITE_CARD_LT
FINITE_CART
FINITE_CART_SUBSET_LEMMA
FINITE_CART_UNIV
FINITE_CBALL
FINITE_COLUMNS
FINITE_COMPLEX_ROOTS_UNITY
FINITE_COMPONENTS
FINITE_COUNTABLE
FINITE_COUNTINGS
FINITE_CROSS
FINITE_CYCLES
FINITE_DELETE
FINITE_DELETE_IMP
FINITE_DIFF
FINITE_DIRICHLET_CHARACTERS
FINITE_DIVISORS
FINITE_EMPTY
FINITE_EMPTY_INTERIOR
FINITE_FACES_OF_SIMPLEX
FINITE_FINITE_IMAGE
FINITE_FINITE_PREIMAGE
FINITE_FINITE_PREIMAGE_GENERAL
FINITE_FINITE_UNIONS
FINITE_FUNSPACE
FINITE_FUNSPACE_UNIV
FINITE_HAS_SIZE
FINITE_HAS_SIZE_LEMMA
FINITE_HYPERPLANE_CELLCOMPLEXES
FINITE_HYPERPLANE_CELLS
FINITE_IMAGE
FINITE_IMAGE_EXPAND
FINITE_IMAGE_IMAGE
FINITE_IMAGE_INJ
FINITE_IMAGE_INJ_EQ
FINITE_IMAGE_INJ_GENERAL
FINITE_IMP_BOUNDED
FINITE_IMP_BOUNDED_CONVEX_HULL
FINITE_IMP_CLOSED
FINITE_IMP_CLOSED_IN
FINITE_IMP_COMPACT
FINITE_IMP_COMPACT_CONVEX_HULL
FINITE_IMP_COUNTABLE
FINITE_IMP_NOT_OPEN
FINITE_INDEX_INJ
FINITE_INDEX_INRANGE
FINITE_INDEX_INRANGE_2
FINITE_INDEX_NUMBERS
FINITE_INDEX_NUMSEG
FINITE_INDEX_NUMSEG_SPECIAL
FINITE_INDEX_WORKS
FINITE_INDUCT_DELETE
FINITE_INDUCT_STRONG
FINITE_INJ
FINITE_INSERT
FINITE_INTER
FINITE_INTERVAL_1
FINITE_INTER_COLLINEAR_OPEN_SEGMENTS
FINITE_INTER_NUMSEG
FINITE_INTSEG
FINITE_INTSEG_RESTRICT
FINITE_LEMMA
FINITE_MAX
FINITE_MULTIVECTOR
FINITE_NUMBER_SEGMENT
FINITE_NUMSEG
FINITE_NUMSEG_LE
FINITE_NUMSEG_LT
FINITE_PARTITIONS
FINITE_PARTITIONS_LEMMA
FINITE_PATHS
FINITE_PCROSS
FINITE_PCROSS_EQ
FINITE_PERMUTATIONS
FINITE_POLYHEDRON_EXPOSED_FACES
FINITE_POLYHEDRON_EXTREME_POINTS
FINITE_POLYHEDRON_FACES
FINITE_POLYHEDRON_FACETS
FINITE_POLYTOPE_FACES
FINITE_POLYTOPE_FACETS
FINITE_POWERSET
FINITE_PRODUCT
FINITE_PRODUCT_DEPENDENT
FINITE_RADICALS
FINITE_REAL_INTERVAL
FINITE_RECURSION
FINITE_RECURSION_DELETE
FINITE_RESTRICT
FINITE_RESTRICT_HYPERPLANE_CELLCOMPLEXES
FINITE_RESTRICT_HYPERPLANE_CELLS
FINITE_ROWS
FINITE_SEGMENT
FINITE_SET_AVOID
FINITE_SET_OF_HYPERPLANE_CELLS
FINITE_SET_OF_LIST
FINITE_SIMPLICES
FINITE_SING
FINITE_SPECIAL_DIVISORS
FINITE_SPHERE
FINITE_SPHERE_1
FINITE_STDBASIS
FINITE_SUBCROSS
FINITE_SUBSET
FINITE_SUBSETS_RESTRICT
FINITE_SUBSET_IMAGE
FINITE_SUBSET_IMAGE_IMP
FINITE_SUBSET_PARTITIONS
FINITE_SUM_IMAGE
FINITE_SUPPORT
FINITE_SUPPORT_DELTA
FINITE_TRANSITIVITY_CHAIN
FINITE_TRIANGLE_INTEGER_POINTS
FINITE_UNION
FINITE_UNIONS
FINITE_UNION_IMP
FINITE_scaled_lattice
FINREC
FINREC_1_LEMMA
FINREC_EXISTS_LEMMA
FINREC_FUN
FINREC_FUN_LEMMA
FINREC_SUC_LEMMA
FINREC_UNIQUE_LEMMA
FIRST_CARTAN_THM_DIM_1
FIXED_POINT_INESSENTIAL_SPHERE_MAP
FIXING_SWAPSEQ_DECREASE
FL
FLATTEN_LEMMA
FLOAT_ABS
FLOAT_ADD
FLOAT_ADD_EQ
FLOAT_ADD_NN
FLOAT_ADD_NNv2
FLOAT_ADD_NP
FLOAT_ADD_PN
FLOAT_ADD_PP
FLOAT_ADD_PPv2
FLOAT_EQ
FLOAT_LE
FLOAT_LT
FLOAT_MUL
FLOAT_NEG
FLOAT_NN
FLOAT_POS
FLOAT_POW
FLOAT_SUB
FLOAT_ZERO
FLOOR
FLOOR_DIV_DIV
FLOOR_DIV_EXISTS
FLOOR_DIV_INTERVAL
FLOOR_DOUBLE
FLOOR_DOUBLE_NUM
FLOOR_EQ_0
FLOOR_FRAC
FLOOR_HALF_INTERVAL
FLOOR_MONO
FLOOR_NUM
FLOOR_NUM_EXISTS
FLOOR_POS
FLOOR_POS_LE
FLOOR_UNIQUE
FLT_LEMMA
FL_RESTRICT
FL_RESTRICTED_SUBSET
FL_SUC
FNIL
FOLLOW_ABS
FOLLOW_LBL
FOLLOW_REL
FOOBAR_LEMMA
FORALL_1
FORALL_2
FORALL_3
FORALL_4
FORALL_ALL
FORALL_AND_THM
FORALL_BOOL_THM
FORALL_CNJ
FORALL_COMPLEX
FORALL_COUNTABLE_AS_IMAGE
FORALL_COUNTABLE_SUBSET_IMAGE
FORALL_CURRY
FORALL_DEST_PLANE
FORALL_DIMINDEX_1
FORALL_DOT_EQ_0
FORALL_DROP
FORALL_DROP_FUN
FORALL_DROP_IMAGE
FORALL_EVENTUALLY
FORALL_FINITE_INDEX
FORALL_FINITE_SUBSET_IMAGE
FORALL_INTEGER
FORALL_IN_CLAUSES
FORALL_IN_CLOSURE
FORALL_IN_DIVISION
FORALL_IN_DIVISION_NONEMPTY
FORALL_IN_GSPEC
FORALL_IN_IMAGE
FORALL_IN_INSERT
FORALL_IN_PCROSS
FORALL_IN_UNIONS
FORALL_LENGTH_CLAUSES
FORALL_LE_def
FORALL_LIFT
FORALL_LIFT_FUN
FORALL_LIFT_IMAGE
FORALL_LINE
FORALL_MULTIVECTOR
FORALL_NEG
FORALL_NOT_THM
FORALL_OF_DROP
FORALL_OF_PASTECART
FORALL_OPTION
FORALL_PAD2D3D_THM
FORALL_PAIRED_THM
FORALL_PAIR_THM
FORALL_PASTECART
FORALL_POINT
FORALL_POS_MONO
FORALL_POS_MONO_1
FORALL_RANGE_SUC
FORALL_REAL
FORALL_REAL_ONE
FORALL_SETCODE
FORALL_SIMP
FORALL_SIMP2
FORALL_SUBSET_IMAGE
FORALL_SUBSET_UNION
FORALL_SUC
FORALL_SUM_THM
FORALL_TRIPLED_THM
FORALL_UNCURRY
FORALL_UNWIND_THM1
FORALL_UNWIND_THM2
FORALL_VALMOD
FORALL_VECTOR_1
FORALL_VECTOR_2
FORALL_VECTOR_3
FORALL_VECTOR_4
FORM
FORM1
FORMSUBST_EQ
FORMSUBST_FV
FORMSUBST_PROPERTIES
FORMSUBST_TRIV
FORMSUBST_TWICE
FORMSUBST_TWICE_GENERAL
FORM_LEMMA1
FORM_LEMMA2
FORM_THM
FORSTER_PUZZLE
FOURIER_COEFFICIENT_ADD
FOURIER_COEFFICIENT_CONST
FOURIER_COEFFICIENT_SUB
FOURIER_DINI_TEST
FOURIER_FEJER_CESARO_SUMMABLE
FOURIER_FEJER_CESARO_SUMMABLE_SIMPLE
FOURIER_JORDAN_BOUNDED_VARIATION
FOURIER_JORDAN_BOUNDED_VARIATION_SIMPLE
FOURIER_OFFSET_TERM
FOURIER_PRODUCTS_INTEGRABLE
FOURIER_PRODUCTS_INTEGRABLE_STRONG
FOURIER_SERIES_L2
FOURIER_SERIES_L2_SUMMABLE
FOURIER_SERIES_L2_SUMMABLE_STRONG
FOURIER_SERIES_SQUARE_SUMMABLE
FOURIER_SUM_0
FOURIER_SUM_0_EXPLICIT
FOURIER_SUM_0_INTEGRAL
FOURIER_SUM_0_INTEGRALS
FOURIER_SUM_LIMIT_DIRICHLET_KERNEL
FOURIER_SUM_LIMIT_DIRICHLET_KERNEL_HALF
FOURIER_SUM_LIMIT_DIRICHLET_KERNEL_PART
FOURIER_SUM_LIMIT_FEJER_KERNEL_HALF
FOURIER_SUM_LIMIT_PAIR
FOURIER_SUM_LIMIT_SINE_PART
FOURIER_SUM_OFFSET
FOURIER_SUM_OFFSET_DIRICHLET_KERNEL
FOURIER_SUM_OFFSET_DIRICHLET_KERNEL_HALF
FOURIER_SUM_OFFSET_FEJER_KERNEL_HALF
FOURIER_SUM_OFFSET_UNPAIRED
FO_LEM
FO_LEMMA1
FRAC_FLOOR
FRAC_NUM
FRAC_UNIQUE
FRECHET_DERIVATIVE_AT
FRECHET_DERIVATIVE_CONST_AT
FRECHET_DERIVATIVE_UNIQUE_AT
FRECHET_DERIVATIVE_UNIQUE_WITHIN
FRECHET_DERIVATIVE_UNIQUE_WITHIN_CLOSED_INTERVAL
FRECHET_DERIVATIVE_UNIQUE_WITHIN_OPEN_INTERVAL
FRECHET_DERIVATIVE_WITHIN_CLOSED_INTERVAL
FRECHET_DERIVATIVE_WORKS
FREEFORM
FREEFORM1
FREEFORM_LEMMA1
FREEFORM_LEMMA2
FREEFORM_THM
FREETERM
FREETERM1
FREETERM_LEMMA1
FREETERM_LEMMA2
FREETERM_THM
FRIENDSHIP
FROM_0
FROM_INTER_NUMSEG
FROM_INTER_NUMSEG_GEN
FRONTIER_BALL
FRONTIER_BIJECTIVE_LINEAR_IMAGE
FRONTIER_CBALL
FRONTIER_CLOSED
FRONTIER_CLOSED_INTERVAL
FRONTIER_CLOSURES
FRONTIER_CLOSURE_CONVEX
FRONTIER_COMPLEMENT
FRONTIER_CONVEX_HULL_CASES
FRONTIER_CONVEX_HULL_EXPLICIT
FRONTIER_DISJOINT_EQ
FRONTIER_EMPTY
FRONTIER_EQ_EMPTY
FRONTIER_FRONTIER_FRONTIER
FRONTIER_FRONTIER_SUBSET
FRONTIER_HALFSPACE_GE
FRONTIER_HALFSPACE_GT
FRONTIER_HALFSPACE_LE
FRONTIER_HALFSPACE_LT
FRONTIER_INJECTIVE_LINEAR_IMAGE
FRONTIER_INSIDE_SUBSET
FRONTIER_INTERIORS
FRONTIER_INTER_SUBSET
FRONTIER_MINIMAL_SEPARATING_CLOSED
FRONTIER_NOT_EMPTY
FRONTIER_OF_COMPONENTS_CLOSED_COMPLEMENT
FRONTIER_OF_COMPONENTS_SUBSET
FRONTIER_OF_CONNECTED_COMPONENT_SUBSET
FRONTIER_OF_CONVEX_HULL
FRONTIER_OF_TRIANGLE
FRONTIER_OPEN_INTERVAL
FRONTIER_OUTSIDE_SUBSET
FRONTIER_RETRACT_OF_PUNCTURED_UNIVERSE
FRONTIER_SING
FRONTIER_STRADDLE
FRONTIER_SUBSET_CLOSED
FRONTIER_SUBSET_COMPACT
FRONTIER_SUBSET_EQ
FRONTIER_SUBSET_RETRACTION
FRONTIER_SURJECTIVE_LINEAR_IMAGE
FRONTIER_TRANSLATION
FRONTIER_UNION
FRONTIER_UNIONS_SUBSET_CLOSURE
FRONTIER_UNION_SUBSET
FRONTIER_UNIV
FRUSTUM_DEGENERATE
FST
FSTCART_ADD
FSTCART_CMUL
FSTCART_NEG
FSTCART_PASTECART
FSTCART_SUB
FSTCART_VEC
FSTCART_VSUM
FST_DEF
FST_VAR
FTA
FTC1
FUBINI_CLOSED_INTERVAL
FUBINI_SIMPLE
FUBINI_SIMPLE_ALT
FUBINI_SIMPLE_COMPACT
FUBINI_SIMPLE_COMPACT_STRONG
FUBINI_SIMPLE_CONVEX
FUBINI_SIMPLE_CONVEX_STRONG
FUBINI_SIMPLE_LEMMA
FUBINI_SIMPLE_OPEN
FUBINI_SIMPLE_OPEN_STRONG
FULL_RANK_INJECTIVE
FULL_RANK_SURJECTIVE
FUN
FUNCTION_CONVERGENT_SUBSEQUENCE
FUNCTION_FACTORS_LEFT
FUNCTION_FACTORS_LEFT_GEN
FUNCTION_FACTORS_RIGHT
FUNCTION_FACTORS_RIGHT_GEN
FUNDAMENTAL_THEOREM_OF_ALGEBRA
FUNDAMENTAL_THEOREM_OF_ALGEBRA_ALT
FUNDAMENTAL_THEOREM_OF_CALCULUS
FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR
FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG
FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
FUNSPACE_EMPTY
FUNSPACE_FIXED
FUNSPACE_INHABITED
FUN_EQ_THM
FUN_IN_IMAGE
FUN_SIZE
FV
FVT
FVT_FINITE
FVT_NUMERAL
FVT_PAIR
FV_AXIOM
FV_DIAGONALIZE
FV_DIVIDES
FV_FINITE
FV_FIXPOINT
FV_FORM
FV_FORM1
FV_FREEFORM
FV_FREEFORM1
FV_FREETERM
FV_FREETERM1
FV_GENERALIZE
FV_GNUMERAL
FV_GNUMERAL1
FV_GNUMERAL1'
FV_GSENTENCE
FV_HSENTENCE
FV_PRIME
FV_PRIMEPOW
FV_PRIMREC
FV_PRIMRECSTEP
FV_PROV
FV_PROV1
FV_QDIAG
FV_QSUBST
FV_RTC
FV_RTCP
FV_SUBSET_VARS
FV_TERM
FV_TERM1
FiveMovesOrLess
FiveMovesOrLess_STRONG
FourMovesToCorrectTwo
FourStepMoveAB
FourStepMoveABBAreach
f(n1,n2)
f_thm
face_of
facet_of
factor_neg_even_neg
factor_neg_even_pos
factor_neg_even_zero
factor_neg_odd_neg
factor_neg_odd_pos
factor_neg_odd_zero
factor_pos_neg
factor_pos_pos
factor_pos_zero
factor_zero_neg
factor_zero_pos
factor_zero_zero
false_def
fejer_kernel
fib
fib2
fibre2
fibre_card
fine
finite_LB
finite_UB
finite_augment
finite_augment1
finite_cls
finite_compact
finite_graph_edge
finite_graph_vertex
finite_index
finite_inf
finite_inf_min
finite_inters
finite_num_closure
finite_set_lower
finite_subset
finite_supm
finite_supm_max
fixpoint
fl
float
floor_abs
floor_add_num
floor_ineq
floor_int
floor_le
floor_level
floor_lt
floor_mono
floor_neg_num
floor_num
floor_range
foo2
forall_thm
forever
form_CASES
form_INDUCT,form_RECURSION
formsubst
formula_thm
fourier_coefficient
frechet_derivative
from
frontier
frustt
frustum
fst_def
fstcart
func
function_on_dyadic_rationals
funspace
fusc
fusc_def
fvs,th1