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
FARKAS_LEMMA
FARKAS_LEMMA_ALT
FASHODA
FASHODA_INTERLACE
FASHODA_UNIT
FASHODA_UNIT_PATH
FINE_DIVISION_EXISTS
FINE_INTER
FINE_INTERS
FINE_SUBSET
FINE_UNION
FINE_UNIONS
FINITELY_GENERATED_CONIC_POLYHEDRON
FINITE_BALL
FINITE_BOUNDED_FUNCTIONS
FINITE_CARD_COMPLEX_ROOTS_UNITY
FINITE_CARD_COMPLEX_ROOTS_UNITY_EXPLICIT
FINITE_CART_SUBSET_LEMMA
FINITE_CBALL
FINITE_COLUMNS
FINITE_COMPLEX_ROOTS_UNITY
FINITE_COMPONENTS
FINITE_EMPTY_INTERIOR
FINITE_FACES_OF_SIMPLEX
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_NOT_OPEN
FINITE_INDEX_NUMSEG_SPECIAL
FINITE_INTERVAL_1
FINITE_INTER_COLLINEAR_OPEN_SEGMENTS
FINITE_INTER_NUMSEG
FINITE_MULTIVECTOR
FINITE_POLYHEDRON_EXPOSED_FACES
FINITE_POLYHEDRON_EXTREME_POINTS
FINITE_POLYHEDRON_FACES
FINITE_POLYHEDRON_FACETS
FINITE_POLYTOPE_FACES
FINITE_POLYTOPE_FACETS
FINITE_ROWS
FINITE_SEGMENT
FINITE_SET_AVOID
FINITE_SIMPLICES
FINITE_SPHERE
FINITE_SPHERE_1
FINITE_STDBASIS
FIRST_CARTAN_THM_DIM_1
FIXED_POINT_INESSENTIAL_SPHERE_MAP
FORALL_1
FORALL_2
FORALL_3
FORALL_4
FORALL_CNJ
FORALL_COMPLEX
FORALL_DIMINDEX_1
FORALL_DOT_EQ_0
FORALL_DROP
FORALL_DROP_FUN
FORALL_DROP_IMAGE
FORALL_EVENTUALLY
FORALL_IN_CLOSURE
FORALL_IN_DIVISION
FORALL_IN_DIVISION_NONEMPTY
FORALL_LIFT
FORALL_LIFT_FUN
FORALL_LIFT_IMAGE
FORALL_MULTIVECTOR
FORALL_OF_DROP
FORALL_OF_PASTECART
FORALL_OPTION
FORALL_PAD2D3D_THM
FORALL_POS_MONO
FORALL_POS_MONO_1
FORALL_REAL
FORALL_REAL_ONE
FORALL_SETCODE
FORALL_SUC
FORALL_VECTOR_1
FORALL_VECTOR_2
FORALL_VECTOR_3
FORALL_VECTOR_4
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
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
FSTCART_ADD
FSTCART_CMUL
FSTCART_NEG
FSTCART_SUB
FSTCART_VEC
FSTCART_VSUM
FTA
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
FUNCTION_CONVERGENT_SUBSEQUENCE
FUNDAMENTAL_THEOREM_OF_CALCULUS
FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR
FUNDAMENTAL_THEOREM_OF_CALCULUS_INTERIOR_STRONG
FUNDAMENTAL_THEOREM_OF_CALCULUS_STRONG
face_of
facet_of
fine
frechet_derivative
from
frontier
frustt
frustum
function_on_dyadic_rationals