HOL html

Files Index

Theorems Index

L (theorems)

L1_LE_NORM
LAMBDA_ADD_GALOIS
LAMBDA_BETA_PERM
LAMBDA_PAIR
LAMBDA_SKOLEM
LAMBDA_SWAP_GALOIS
LANDAU_PICARD
LAW_OF_COSINES
LAW_OF_SINES
LEBESGUE_COVERING_LEMMA
LEBESGUE_DENSITY_THEOREM
LEBESGUE_MEASURABLE_CLOSED
LEBESGUE_MEASURABLE_COMPACT
LEBESGUE_MEASURABLE_COMPL
LEBESGUE_MEASURABLE_CONTINUOUS_IMAGE
LEBESGUE_MEASURABLE_CONVEX
LEBESGUE_MEASURABLE_COUNTABLE_INTERS
LEBESGUE_MEASURABLE_COUNTABLE_INTERS_EXPLICIT
LEBESGUE_MEASURABLE_COUNTABLE_UNIONS
LEBESGUE_MEASURABLE_COUNTABLE_UNIONS_EXPLICIT
LEBESGUE_MEASURABLE_DIFF
LEBESGUE_MEASURABLE_DIFFERENTIABLE_IMAGE
LEBESGUE_MEASURABLE_EMPTY
LEBESGUE_MEASURABLE_IFF_MEASURABLE
LEBESGUE_MEASURABLE_INNER_CLOSED
LEBESGUE_MEASURABLE_INTER
LEBESGUE_MEASURABLE_INTERS
LEBESGUE_MEASURABLE_INTERVAL
LEBESGUE_MEASURABLE_JORDAN
LEBESGUE_MEASURABLE_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
LEBESGUE_MEASURABLE_LEBESGUE_MEASURABLE_PREIMAGE_OPEN
LEBESGUE_MEASURABLE_LINEAR_IMAGE_EQ
LEBESGUE_MEASURABLE_ON_SUBINTERVALS
LEBESGUE_MEASURABLE_OPEN
LEBESGUE_MEASURABLE_OUTER_OPEN
LEBESGUE_MEASURABLE_PREIMAGE_CLOSED
LEBESGUE_MEASURABLE_PREIMAGE_OPEN
LEBESGUE_MEASURABLE_REGULAR_INNER
LEBESGUE_MEASURABLE_REGULAR_OUTER
LEBESGUE_MEASURABLE_TRANSLATION
LEBESGUE_MEASURABLE_UNION
LEBESGUE_MEASURABLE_UNIONS
LEBESGUE_MEASURABLE_UNIV
LEFT_INVERSE_LINEAR
LEFT_INVERTIBLE_TRANSP
LEFT_RIGHT_INVERSE_EQ
LEFT_RIGHT_INVERSE_LINEAR
LEMMA
LEMMA1
LEMMA2
LEMMA3
LEMMA_1
LEMMA_1_ALT
LEMMA_2
LEMMA_ZERO
LENGTH_LINEAR_IMAGE
LENGTH_TRANSLATION
LHOSPITAL
LIFT_ADD
LIFT_CMUL
LIFT_COMPONENT
LIFT_DROP
LIFT_EQ
LIFT_EQ_CMUL
LIFT_INTEGRAL_COMPONENT
LIFT_IN_IMAGE_LIFT
LIFT_NEG
LIFT_NUM
LIFT_SUB
LIFT_SUM
LIM
LIMIT_POINT_FINITE
LIMIT_POINT_OF_SPHERE
LIMIT_POINT_UNION
LIMPT_APPROACHABLE
LIMPT_APPROACHABLE_LE
LIMPT_APPROACHABLE_LIFT
LIMPT_BALL
LIMPT_EMPTY
LIMPT_INJECTIVE_LINEAR_IMAGE_EQ
LIMPT_INSERT
LIMPT_OF_CLOSURE
LIMPT_OF_CONDENSATION_POINTS
LIMPT_OF_CONVEX
LIMPT_OF_LIMPTS
LIMPT_OF_OPEN
LIMPT_OF_OPEN_IN
LIMPT_OF_SEQUENCE_SUBSEQUENCE
LIMPT_OF_UNIV
LIMPT_PCROSS
LIMPT_SEQUENTIAL
LIMPT_SEQUENTIAL_INJ
LIMPT_SING
LIMPT_SUBSET
LIMPT_TRANSLATION_EQ
LIMPT_UNIV
LIM_1_OVER_LOG
LIM_1_OVER_N
LIM_1_OVER_POWER
LIM_ABS
LIM_ADD
LIM_AT
LIM_ATREAL
LIM_ATREAL_AT
LIM_ATREAL_ATCOMPLEX
LIM_ATREAL_WITHINREAL
LIM_AT_ID
LIM_AT_INFINITY
LIM_AT_NEGINFINITY
LIM_AT_POSINFINITY
LIM_AT_WITHIN
LIM_AT_ZERO
LIM_BILINEAR
LIM_CASES_COFINITE_SEQUENTIALLY
LIM_CASES_FINITE_SEQUENTIALLY
LIM_CASES_SEQUENTIALLY
LIM_CEXP_MINUS_1
LIM_CMUL
LIM_CMUL_EQ
LIM_CNJ
LIM_COMPLEX_DIV
LIM_COMPLEX_INV
LIM_COMPLEX_LMUL
LIM_COMPLEX_MUL
LIM_COMPLEX_POW
LIM_COMPLEX_REAL
LIM_COMPLEX_REAL_0
LIM_COMPLEX_RMUL
LIM_COMPONENT
LIM_COMPONENTWISE
LIM_COMPONENTWISE_LIFT
LIM_COMPONENT_EQ
LIM_COMPONENT_LBOUND
LIM_COMPONENT_LE
LIM_COMPONENT_UBOUND
LIM_COMPOSE_AT
LIM_COMPOSE_WITHIN
LIM_CONG_AT
LIM_CONG_ATREAL
LIM_CONG_WITHIN
LIM_CONG_WITHINREAL
LIM_CONST
LIM_CONST_EQ
LIM_CONTINUOUS
LIM_CONTINUOUS_FUNCTION
LIM_DROP_LBOUND
LIM_DROP_LE
LIM_DROP_UBOUND
LIM_EVENTUALLY
LIM_IM_LBOUND
LIM_IM_UBOUND
LIM_INFINITY_SEQUENTIALLY_COMPLEX
LIM_INV
LIM_INV_N
LIM_IN_CLOSED_SET
LIM_LIFT_DOT
LIM_LINEAR
LIM_LOG_OVER_N
LIM_LOG_OVER_POWER
LIM_MAX
LIM_MIN
LIM_MUL
LIM_MUL_NORM_WITHIN
LIM_NEG
LIM_NEG_EQ
LIM_NORM
LIM_NORM_LBOUND
LIM_NORM_UBOUND
LIM_NULL
LIM_NULL_CMUL_BOUNDED
LIM_NULL_CMUL_EQ
LIM_NULL_COMPARISON
LIM_NULL_COMPARISON_COMPLEX
LIM_NULL_COMPARISON_COMPLEX_RE
LIM_NULL_COMPLEX_ADD
LIM_NULL_COMPLEX_BOUND
LIM_NULL_COMPLEX_LMUL
LIM_NULL_COMPLEX_LMUL_BOUNDED
LIM_NULL_COMPLEX_MUL
LIM_NULL_COMPLEX_NEG
LIM_NULL_COMPLEX_POW
LIM_NULL_COMPLEX_POW_EQ
LIM_NULL_COMPLEX_RMUL
LIM_NULL_COMPLEX_RMUL_BOUNDED
LIM_NULL_COMPLEX_SUB
LIM_NULL_NORM
LIM_NULL_VMUL_BOUNDED
LIM_N_OVER_POWN
LIM_N_TIMES_POWN
LIM_PASTECART
LIM_PASTECART_EQ
LIM_POSINFINITY_SEQUENTIALLY
LIM_POWN
LIM_REAL_CONTINUOUS_FUNCTION
LIM_RE_LBOUND
LIM_RE_UBOUND
LIM_SEQUENTIALLY
LIM_SUB
LIM_SUBSEQUENCE
LIM_TRANSFORM
LIM_TRANSFORM_AT
LIM_TRANSFORM_AWAY_AT
LIM_TRANSFORM_AWAY_WITHIN
LIM_TRANSFORM_BOUND
LIM_TRANSFORM_EQ
LIM_TRANSFORM_EVENTUALLY
LIM_TRANSFORM_WITHIN
LIM_TRANSFORM_WITHINREAL_SET
LIM_TRANSFORM_WITHIN_OPEN
LIM_TRANSFORM_WITHIN_SET
LIM_UNION
LIM_UNION_UNIV
LIM_UNIQUE
LIM_VMUL
LIM_VSUM
LIM_WITHIN
LIM_WITHINREAL
LIM_WITHINREAL_LE
LIM_WITHINREAL_SUBSET
LIM_WITHINREAL_WITHIN
LIM_WITHINREAL_WITHINCOMPLEX
LIM_WITHIN_CLOSED_TRIVIAL
LIM_WITHIN_EMPTY
LIM_WITHIN_ID
LIM_WITHIN_INTERIOR
LIM_WITHIN_LE
LIM_WITHIN_OPEN
LIM_WITHIN_REAL_OPEN
LIM_WITHIN_SUBSET
LIM_WITHIN_UNION
LIM_ZERO_INFINITY_COMPLEX
LIM_ZERO_NEGINFINITY
LIM_ZERO_POSINFINITY
LINDELOF
LINDELOF_OPEN_IN
LINEAR_0
LINEAR_1
LINEAR_ADD
LINEAR_BIJECTIVE_DIMINDEX_EQ
LINEAR_BIJECTIVE_LEFT_RIGHT_INVERSE
LINEAR_BOUNDED
LINEAR_BOUNDED_POS
LINEAR_CMUL
LINEAR_CNJ
LINEAR_COMPLEX_MUL
LINEAR_COMPONENTWISE
LINEAR_COMPONENTWISE_EXPANSION
LINEAR_COMPOSE
LINEAR_COMPOSE_ADD
LINEAR_COMPOSE_CMUL
LINEAR_COMPOSE_NEG
LINEAR_COMPOSE_SUB
LINEAR_COMPOSE_VSUM
LINEAR_CONTINUOUS_AT
LINEAR_CONTINUOUS_COMPOSE
LINEAR_CONTINUOUS_ON
LINEAR_CONTINUOUS_ON_COMPOSE
LINEAR_CONTINUOUS_WITHIN
LINEAR_CX_IM
LINEAR_CX_RE
LINEAR_DROPOUT
LINEAR_EQ
LINEAR_EQ_0
LINEAR_EQ_0_SPAN
LINEAR_EQ_MATRIX
LINEAR_EQ_MBASIS
LINEAR_EQ_STDBASIS
LINEAR_FRECHET_DERIVATIVE
LINEAR_FROM_REALS
LINEAR_FSTCART
LINEAR_I
LINEAR_ID
LINEAR_IMAGE_SUBSET_INTERIOR
LINEAR_INDEPENDENT_EXTEND
LINEAR_INDEPENDENT_EXTEND_LEMMA
LINEAR_INDEP_IMAGE_LEMMA
LINEAR_INJECTIVE_0
LINEAR_INJECTIVE_0_SUBSPACE
LINEAR_INJECTIVE_BOUNDED_BELOW_POS
LINEAR_INJECTIVE_DIMINDEX_LE
LINEAR_INJECTIVE_IMP_SURJECTIVE
LINEAR_INJECTIVE_ISOMORPHISM
LINEAR_INJECTIVE_LEFT_INVERSE
LINEAR_INTERIOR_IMAGE_SUBSET
LINEAR_INVERSE_LEFT
LINEAR_INVERTIBLE_BOUNDED_BELOW
LINEAR_INVERTIBLE_BOUNDED_BELOW_POS
LINEAR_LIFT_COMPONENT
LINEAR_LIFT_DOT
LINEAR_LIM_0
LINEAR_MATRIX_EXISTS
LINEAR_NEG
LINEAR_NEGATION
LINEAR_OPEN_MAPPING
LINEAR_PAD2D3D
LINEAR_PASTECART
LINEAR_PROPERTY
LINEAR_REFLECT_ALONG
LINEAR_ROTATE2D
LINEAR_SCALING
LINEAR_SINGULAR_IMAGE_HYPERPLANE
LINEAR_SINGULAR_INTO_HYPERPLANE
LINEAR_SNDCART
LINEAR_SUB
LINEAR_SUBSPACE_GRAPH
LINEAR_SURJECTIVE_DIMINDEX_LE
LINEAR_SURJECTIVE_IFF_INJECTIVE
LINEAR_SURJECTIVE_IMP_INJECTIVE
LINEAR_SURJECTIVE_ISOMORPHISM
LINEAR_SURJECTIVE_RIGHT_INVERSE
LINEAR_TO_REALS
LINEAR_UNIFORMLY_CONTINUOUS_ON
LINEAR_VMUL_COMPONENT
LINEAR_VMUL_DROP
LINEAR_VSUM
LINEAR_VSUM_MUL
LINEAR_ZERO
LINEPATH_CX
LINEPATH_IN_PATH
LINEPATH_LINEAR_IMAGE
LINEPATH_REFL
LINEPATH_TRANSLATION
LIOUVILLE_THEOREM
LIOUVILLE_WEAK
LIOUVILLE_WEAK_INVERSE
LIPSCHITZ_REAL_POLYNOMIAL_FUNCTION
LIPSCHITZ_VECTOR_POLYNOMIAL_FUNCTION
LITTLE_PICARD
LOCALLY_CLOSED
LOCALLY_COMPACT
LOCALLY_COMPACT_CLOSED_IN
LOCALLY_COMPACT_CLOSED_IN_OPEN
LOCALLY_COMPACT_HOMEOMORPHIC_CLOSED
LOCALLY_COMPACT_HOMEOMORPHISM_PROJECTION_CLOSED
LOCALLY_COMPACT_INTER
LOCALLY_COMPACT_LINEAR_IMAGE_EQ
LOCALLY_COMPACT_OPEN_IN
LOCALLY_COMPACT_OPEN_INTER_CLOSURE
LOCALLY_COMPACT_TRANSLATION_EQ
LOCALLY_COMPACT_UNIV
LOCALLY_CONNECTED_COMPONENTS
LOCALLY_CONNECTED_CONNECTED_COMPONENT
LOCALLY_CONNECTED_CONTINUOUS_IMAGE_COMPACT
LOCALLY_CONNECTED_IM_KLEINEN
LOCALLY_CONNECTED_LEFT_INVERTIBLE_IMAGE
LOCALLY_CONNECTED_LINEAR_IMAGE_EQ
LOCALLY_CONNECTED_OPEN_COMPONENT
LOCALLY_CONNECTED_PATH_IMAGE
LOCALLY_CONNECTED_PCROSS
LOCALLY_CONNECTED_PCROSS_EQ
LOCALLY_CONNECTED_QUOTIENT_IMAGE
LOCALLY_CONNECTED_RIGHT_INVERTIBLE_IMAGE
LOCALLY_CONNECTED_SPHERE
LOCALLY_CONNECTED_SPHERE_GEN
LOCALLY_CONNECTED_TRANSLATION_EQ
LOCALLY_CONNECTED_UNIV
LOCALLY_DIFF_CLOSED
LOCALLY_EMPTY
LOCALLY_INJECTIVE_LINEAR_IMAGE
LOCALLY_INTER
LOCALLY_MONO
LOCALLY_OPEN_MAP_IMAGE
LOCALLY_OPEN_SUBSET
LOCALLY_PATH_CONNECTED_COMPONENTS
LOCALLY_PATH_CONNECTED_CONNECTED_COMPONENT
LOCALLY_PATH_CONNECTED_CONTINUOUS_IMAGE_COMPACT
LOCALLY_PATH_CONNECTED_IMP_LOCALLY_CONNECTED
LOCALLY_PATH_CONNECTED_IM_KLEINEN
LOCALLY_PATH_CONNECTED_LEFT_INVERTIBLE_IMAGE
LOCALLY_PATH_CONNECTED_LINEAR_IMAGE_EQ
LOCALLY_PATH_CONNECTED_PATH_COMPONENT
LOCALLY_PATH_CONNECTED_PATH_IMAGE
LOCALLY_PATH_CONNECTED_PCROSS
LOCALLY_PATH_CONNECTED_PCROSS_EQ
LOCALLY_PATH_CONNECTED_QUOTIENT_IMAGE
LOCALLY_PATH_CONNECTED_RIGHT_INVERTIBLE_IMAGE
LOCALLY_PATH_CONNECTED_SPHERE
LOCALLY_PATH_CONNECTED_SPHERE_GEN
LOCALLY_PATH_CONNECTED_TRANSLATION_EQ
LOCALLY_PATH_CONNECTED_UNIV
LOCALLY_PCROSS
LOCALLY_SING
LOCALLY_TRANSLATION
LOG_1
LOG_DIV
LOG_EXP
LOG_INJ
LOG_INV
LOG_LE
LOG_LT_X
LOG_MONO_LE
LOG_MONO_LE_IMP
LOG_MONO_LT
LOG_MONO_LT_IMP
LOG_MUL
LOG_POS
LOG_POS_LT
LOG_POW
LOG_ROOT
LOWDIM_EQ_HYPERPLANE
LOWDIM_EXPAND_BASIS
LOWDIM_EXPAND_DIMENSION
LOWDIM_SUBSET_HYPERPLANE
LOWER_BOUND_FINITE_SET
LOWER_BOUND_FINITE_SET_REAL
LUZIN
lambdas
lebesgue_measurable
lemma
lemma0
lemma1
lemma2
lemma3
lemma4
lift
lifted
lim
limit_point_of
lin_combo
linear
linepath
locally
log_def