HOL html

Files Index

Theorems Index

M (theorems)

MATRIX_ADD_AC
MATRIX_ADD_ASSOC
MATRIX_ADD_COMPONENT
MATRIX_ADD_LDISTRIB
MATRIX_ADD_LID
MATRIX_ADD_LNEG
MATRIX_ADD_RDISTRIB
MATRIX_ADD_RID
MATRIX_ADD_RNEG
MATRIX_ADD_SYM
MATRIX_ADJOINT
MATRIX_CMUL_ADD_LDISTRIB
MATRIX_CMUL_ADD_RDISTRIB
MATRIX_CMUL_ASSOC
MATRIX_CMUL_COMPONENT
MATRIX_CMUL_LID
MATRIX_CMUL_LZERO
MATRIX_CMUL_RZERO
MATRIX_CMUL_SUB_LDISTRIB
MATRIX_CMUL_SUB_RDISTRIB
MATRIX_COMPOSE
MATRIX_EQ
MATRIX_EQUAL_COLUMNS
MATRIX_EQUAL_ROWS
MATRIX_FULL_LINEAR_EQUATIONS
MATRIX_I
MATRIX_ID
MATRIX_INV
MATRIX_INVERTIBLE
MATRIX_INV_COFACTOR
MATRIX_INV_I
MATRIX_INV_MUL
MATRIX_INV_UNIQUE
MATRIX_INV_UNIQUE_LEFT
MATRIX_INV_UNIQUE_RIGHT
MATRIX_LEFT_INVERSE_COFACTOR
MATRIX_LEFT_INVERTIBLE
MATRIX_LEFT_INVERTIBLE_INDEPENDENT_COLUMNS
MATRIX_LEFT_INVERTIBLE_INJECTIVE
MATRIX_LEFT_INVERTIBLE_KER
MATRIX_LEFT_INVERTIBLE_SPAN_ROWS
MATRIX_LEFT_RIGHT_INVERSE
MATRIX_MUL_ASSOC
MATRIX_MUL_COMPONENT
MATRIX_MUL_DOT
MATRIX_MUL_LEFT_COFACTOR
MATRIX_MUL_LID
MATRIX_MUL_LINV
MATRIX_MUL_LMUL
MATRIX_MUL_LNEG
MATRIX_MUL_LTRANSP_DOT_COLUMN
MATRIX_MUL_LZERO
MATRIX_MUL_RID
MATRIX_MUL_RIGHT_COFACTOR
MATRIX_MUL_RINV
MATRIX_MUL_RMUL
MATRIX_MUL_RNEG
MATRIX_MUL_RTRANSP_DOT_ROW
MATRIX_MUL_RZERO
MATRIX_MUL_VSUM
MATRIX_MUL_VSUM_ALT
MATRIX_NEG_0
MATRIX_NEG_ADD
MATRIX_NEG_COMPONENT
MATRIX_NEG_EQ_0
MATRIX_NEG_MINUS1
MATRIX_NEG_NEG
MATRIX_NEG_SUB
MATRIX_NONFULL_LINEAR_EQUATIONS
MATRIX_NONFULL_LINEAR_EQUATIONS_EQ
MATRIX_OF_MATRIX_VECTOR_MUL
MATRIX_REFLECT_ALONG_BASIS
MATRIX_RIGHT_INVERSE_COFACTOR
MATRIX_RIGHT_INVERTIBLE
MATRIX_RIGHT_INVERTIBLE_INDEPENDENT_ROWS
MATRIX_RIGHT_INVERTIBLE_SPAN_COLUMNS
MATRIX_RIGHT_INVERTIBLE_SURJECTIVE
MATRIX_ROTATE2D
MATRIX_SELF_ADJOINT
MATRIX_SUB
MATRIX_SUB_COMPONENT
MATRIX_SUB_LDISTRIB
MATRIX_SUB_LZERO
MATRIX_SUB_RDISTRIB
MATRIX_SUB_REFL
MATRIX_SUB_RZERO
MATRIX_TRANSP_MUL
MATRIX_TRIVIAL_LINEAR_EQUATIONS
MATRIX_VECTOR_COLUMN
MATRIX_VECTOR_MUL
MATRIX_VECTOR_MUL_ADD_LDISTRIB
MATRIX_VECTOR_MUL_ADD_RDISTRIB
MATRIX_VECTOR_MUL_ASSOC
MATRIX_VECTOR_MUL_BASIS
MATRIX_VECTOR_MUL_COMPONENT
MATRIX_VECTOR_MUL_INJECTIVE_ON_ROWSPACE
MATRIX_VECTOR_MUL_IN_COLUMNSPACE
MATRIX_VECTOR_MUL_LID
MATRIX_VECTOR_MUL_LINEAR
MATRIX_VECTOR_MUL_LZERO
MATRIX_VECTOR_MUL_RMUL
MATRIX_VECTOR_MUL_RZERO
MATRIX_VECTOR_MUL_SUB_LDISTRIB
MATRIX_VECTOR_MUL_SUB_RDISTRIB
MATRIX_VECTOR_MUL_TRANSP
MATRIX_WLOG_INVERTIBLE
MATRIX_WORKS
MAT_0_COMPONENT
MAT_COMPONENT
MAXIMAL_AFFINE_INDEPENDENT_SUBSET
MAXIMAL_AFFINE_INDEPENDENT_SUBSET_AFFINE
MAXIMAL_INDEPENDENT_SUBSET
MAXIMAL_INDEPENDENT_SUBSET_EXTEND
MAXIMUM_MODULUS_PRINCIPLE
MBASIS_COMPONENT
MBASIS_EQ_0
MBASIS_EXPANSION
MBASIS_EXTENSION
MBASIS_NONZERO
MBASIS_SPLIT
MEASURABLE
MEASURABLE_ADDITIVE_IMP_LINEAR
MEASURABLE_ALMOST
MEASURABLE_BALL
MEASURABLE_BALL_AFF_GT
MEASURABLE_BALL_WEDGE
MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_ABSOLUTELY_INTEGRABLE
MEASURABLE_BOUNDED_BY_INTEGRABLE_IMP_INTEGRABLE
MEASURABLE_BOUNDED_INTER_OPEN
MEASURABLE_CBALL
MEASURABLE_CLOSED_SECTOR_LE
MEASURABLE_CLOSED_SECTOR_LT
MEASURABLE_CLOSED_SECTOR_LTE
MEASURABLE_CLOSURE
MEASURABLE_COMPACT
MEASURABLE_CONIC_CAP
MEASURABLE_CONIC_CAP_WEDGE
MEASURABLE_CONV0
MEASURABLE_CONVEX
MEASURABLE_CONVEX_HULL
MEASURABLE_COUNTABLE_INTERS
MEASURABLE_COUNTABLE_INTERS_GEN
MEASURABLE_COUNTABLE_UNIONS
MEASURABLE_COUNTABLE_UNIONS_BOUNDED
MEASURABLE_COUNTABLE_UNIONS_STRONG
MEASURABLE_DIFF
MEASURABLE_ELEMENTARY
MEASURABLE_ELLIPSOID
MEASURABLE_EMPTY
MEASURABLE_FRONTIER
MEASURABLE_IMP_LEBESGUE_MEASURABLE
MEASURABLE_INNER_COMPACT
MEASURABLE_INNER_OUTER
MEASURABLE_INSERT
MEASURABLE_INSIDE
MEASURABLE_INTEGRABLE
MEASURABLE_INTER
MEASURABLE_INTERIOR
MEASURABLE_INTERVAL
MEASURABLE_INTER_HALFSPACE_GE
MEASURABLE_INTER_HALFSPACE_LE
MEASURABLE_INTER_INTERVAL
MEASURABLE_JORDAN
MEASURABLE_LEGESGUE_MEASURABLE_INTER_MEASURABLE
MEASURABLE_LEGESGUE_MEASURABLE_SUBSET
MEASURABLE_LINEAR_IMAGE
MEASURABLE_LINEAR_IMAGE_EQ
MEASURABLE_LINEAR_IMAGE_INTERVAL
MEASURABLE_MEASURABLE_DIFF_LEGESGUE_MEASURABLE
MEASURABLE_MEASURABLE_INTER_LEGESGUE_MEASURABLE
MEASURABLE_MEASURABLE_PREIMAGE_CLOSED
MEASURABLE_MEASURABLE_PREIMAGE_OPEN
MEASURABLE_MEASURE_EQ_0
MEASURABLE_MEASURE_POS_LT
MEASURABLE_NEGLIGIBLE_SYMDIFF
MEASURABLE_NEGLIGIBLE_SYMDIFF_EQ
MEASURABLE_NESTED_UNIONS
MEASURABLE_NONNEGLIGIBLE_IMP_LARGE
MEASURABLE_ON_0
MEASURABLE_ON_ADD
MEASURABLE_ON_CASES
MEASURABLE_ON_CMUL
MEASURABLE_ON_COMBINE
MEASURABLE_ON_COMPLEX_DIV
MEASURABLE_ON_COMPLEX_INV
MEASURABLE_ON_COMPLEX_MUL
MEASURABLE_ON_COMPONENTWISE
MEASURABLE_ON_COMPOSE_CONTINUOUS
MEASURABLE_ON_COMPOSE_CONTINUOUS_0
MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET
MEASURABLE_ON_COMPOSE_CONTINUOUS_CLOSED_SET_0
MEASURABLE_ON_COMPOSE_CONTINUOUS_OPEN_INTERVAL
MEASURABLE_ON_CONST
MEASURABLE_ON_COUNTABLE_UNIONS
MEASURABLE_ON_DIFF
MEASURABLE_ON_DROP_MUL
MEASURABLE_ON_EMPTY
MEASURABLE_ON_INTER
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_CLOSED_EQ
MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_OPEN_EQ
MEASURABLE_ON_LEBESGUE_MEASURABLE_SUBSET
MEASURABLE_ON_LIFT_MUL
MEASURABLE_ON_LIMIT
MEASURABLE_ON_LINEAR_IMAGE_EQ
MEASURABLE_ON_MAX
MEASURABLE_ON_MEASURABLE_PREIMAGE_CLOSED_EQ
MEASURABLE_ON_MEASURABLE_PREIMAGE_OPEN_EQ
MEASURABLE_ON_MEASURABLE_SUBSET
MEASURABLE_ON_MIN
MEASURABLE_ON_NEG
MEASURABLE_ON_NEG_EQ
MEASURABLE_ON_NORM
MEASURABLE_ON_PASTECART
MEASURABLE_ON_PREIMAGE_CLOSED
MEASURABLE_ON_PREIMAGE_CLOSED_INTERVAL
MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GE
MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_GT
MEASURABLE_ON_PREIMAGE_OPEN_HALFSPACE_COMPONENT_LE
MEASURABLE_ON_RESTRICT
MEASURABLE_ON_SPIKE
MEASURABLE_ON_SPIKE_SET
MEASURABLE_ON_SUB
MEASURABLE_ON_TRANSLATION
MEASURABLE_ON_TRANSLATION_EQ
MEASURABLE_ON_UNION
MEASURABLE_ON_UNIONS
MEASURABLE_ON_UNIV
MEASURABLE_ON_VECTOR_DERIVATIVE
MEASURABLE_ON_VSUM
MEASURABLE_OPEN
MEASURABLE_OUTER_CLOSED_INTERVALS
MEASURABLE_OUTER_INTERVALS_BOUNDED
MEASURABLE_OUTER_INTERVALS_BOUNDED_EXPLICIT_SPECIAL
MEASURABLE_OUTER_OPEN
MEASURABLE_OUTER_OPEN_INTERVALS
MEASURABLE_RULES
MEASURABLE_SCALING
MEASURABLE_SCALING_EQ
MEASURABLE_SIMPLEX
MEASURABLE_SMALL_IMP_NEGLIGIBLE
MEASURABLE_TETRAHEDRON
MEASURABLE_TRANSLATION
MEASURABLE_TRANSLATION_EQ
MEASURABLE_TRIANGLE
MEASURABLE_UNION
MEASURABLE_UNIONS
MEASURE_BALL_AFF_GT_SHUFFLE
MEASURE_BALL_AFF_GT_SHUFFLE_LEMMA
MEASURE_BALL_BOUND
MEASURE_BALL_POS
MEASURE_CBALL_BOUND
MEASURE_CBALL_POS
MEASURE_CLOSED_SECTOR_LE
MEASURE_CLOSURE
MEASURE_CONV0_CONVEX_HULL
MEASURE_COUNTABLE_UNIONS_APPROACHABLE
MEASURE_COUNTABLE_UNIONS_LE
MEASURE_COUNTABLE_UNIONS_LE_GEN
MEASURE_COUNTABLE_UNIONS_LE_STRONG
MEASURE_COUNTABLE_UNIONS_LE_STRONG_GEN
MEASURE_DIFF_SUBSET
MEASURE_DISJOINT_UNION
MEASURE_DISJOINT_UNIONS
MEASURE_DISJOINT_UNIONS_IMAGE
MEASURE_DISJOINT_UNIONS_IMAGE_STRONG
MEASURE_DISJOINT_UNION_EQ
MEASURE_ELEMENTARY
MEASURE_ELLIPSOID
MEASURE_EMPTY
MEASURE_EQ_0
MEASURE_FRONTIER
MEASURE_INSERT
MEASURE_INTEGRAL
MEASURE_INTEGRAL_UNIV
MEASURE_INTERIOR
MEASURE_INTERVAL
MEASURE_INTERVAL_1
MEASURE_INTERVAL_1_ALT
MEASURE_INTERVAL_2
MEASURE_INTERVAL_2_ALT
MEASURE_INTERVAL_3
MEASURE_INTERVAL_3_ALT
MEASURE_INTERVAL_4
MEASURE_INTERVAL_4_ALT
MEASURE_LIMIT
MEASURE_LINEAR_IMAGE
MEASURE_LINEAR_IMAGE_SAME
MEASURE_LUNE_DECOMPOSITION
MEASURE_NEGLIGIBLE_SYMDIFF
MEASURE_NEGLIGIBLE_UNION
MEASURE_NEGLIGIBLE_UNIONS
MEASURE_NEGLIGIBLE_UNIONS_IMAGE
MEASURE_NEGLIGIBLE_UNIONS_IMAGE_STRONG
MEASURE_NEGLIGIBLE_UNION_EQ
MEASURE_OPEN_POS_LT
MEASURE_OPEN_SECTOR_LT
MEASURE_ORTHOGONAL_IMAGE_EQ
MEASURE_POS_LE
MEASURE_SCALE
MEASURE_SCALING
MEASURE_SIMPLEX
MEASURE_SUBSET
MEASURE_TETRAHEDRON
MEASURE_TRANSLATION
MEASURE_TRIANGLE
MEASURE_UNION
MEASURE_UNIONS_LE
MEASURE_UNIONS_LE_IMAGE
MEASURE_UNION_LE
MEASURE_UNIQUE
MEM_LINEAR_IMAGE
MEM_TRANSLATION
MIDPOINTS_IN_CONVEX_HULL
MIDPOINT_BETWEEN
MIDPOINT_COLLINEAR
MIDPOINT_CONVEX_DYADIC_RATIONALS
MIDPOINT_EQ_ENDPOINT
MIDPOINT_IN_SEGMENT
MIDPOINT_LINEAR_IMAGE
MIDPOINT_REFL
MIDPOINT_SYM
MINIMAL_IN_INSERT
MOEBIUS_FUNCTION_COMPOSE
MOEBIUS_FUNCTION_EQ_ZERO
MOEBIUS_FUNCTION_HOLOMORPHIC
MOEBIUS_FUNCTION_NORM_LT_1
MOEBIUS_FUNCTION_OF_ZERO
MOEBIUS_FUNCTION_SIMPLE
MONODROMY_CONTINUOUS_LOG
MONOIDAL_AND
MONOIDAL_COMPLEX_MUL
MONOIDAL_LIFTED
MONOIDAL_VECTOR_ADD
MONOTONE_BIGGER
MONOTONE_CONVERGENCE_DECREASING
MONOTONE_CONVERGENCE_INCREASING
MONOTONE_CONVERGENCE_INTERVAL
MONOTONE_SUBSEQUENCE
MONTEL
MORERA_LOCAL_TRIANGLE
MORERA_LOCAL_TRIANGLE_GEN
MORERA_TRIANGLE
MULTIVECTOR_ADD_COMPONENT
MULTIVECTOR_BETA
MULTIVECTOR_EQ
MULTIVECTOR_ETA
MULTIVECTOR_GRADE
MULTIVECTOR_IMAGE
MULTIVECTOR_MUL_COMPONENT
MULTIVECTOR_UNIQUE
MULTIVECTOR_VEC_COMPONENT
MULTIVECTOR_VSUM
MULTIVECTOR_VSUM_COMPONENT
MVT
MVT_GENERAL
MVT_SIMPLE
MVT_VERY_SIMPLE
mat
matrix
matrix_add
matrix_cmul
matrix_inv
matrix_mul
matrix_neg
matrix_sub
matrix_vector_mul
mbasis
measurable
measurable_on
measure
memma
midpoint
moebius_function
multivec
multivector
multivector_tybij_th