HOL html

Files Index

Theorems Index

M (theorems)

MAGIC_DERIVATIVE
MAINTHM_A
MAINTHM_B
MAIN_RESULT
MANGOLDT
MANGOLDT_1
MANGOLDT_LOG_SUM
MANGOLDT_POS
MANGOLDT_POS_LE
MANGOLDT_PRIMEPOW
MAP
MAP2
MAP2_DEF
MAP2_EL
MAP2_EL_LEM
MAP_APPEND
MAP_EQ
MAP_EQ_ALL2
MAP_EQ_DEGEN
MAP_EQ_NIL
MAP_FST_ZIP
MAP_I
MAP_ID
MAP_REVERSE
MAP_SND_ZIP
MAP_o
MATCH_SEQPATTERN
MATINSERT_THM
MATINSERT_THM2
MATRIC_CHARPOLY_DIFFERENCE
MATRIC_POLYFUN_EQ_0
MATRIC_POLY_LEMMA
MATRIC_POWER_DIFFERENCE
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_BY_CRAMER
MATRIX_BY_CRAMER_LEMMA
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_LEMMA
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_3
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
MAX
MAXIMAL_AFFINE_INDEPENDENT_SUBSET
MAXIMAL_AFFINE_INDEPENDENT_SUBSET_AFFINE
MAXIMAL_INDEPENDENT_SUBSET
MAXIMAL_INDEPENDENT_SUBSET_EXTEND
MAXIMUM_MODULUS_PRINCIPLE
MAXL
MAXL_LE
MAX_0
MAX_ABS_DEF
MAX_ABS_LE
MAX_ACI
MAX_ASSOC
MAX_LE
MAX_LEMMA
MAX_LT
MAX_SYM
MAY_LEMMA
MBASIS_COMPONENT
MBASIS_EQ_0
MBASIS_EXPANSION
MBASIS_EXTENSION
MBASIS_NONZERO
MBASIS_SPLIT
MCLAURIN
MCLAURIN_ALL_LE
MCLAURIN_ALL_LT
MCLAURIN_ATN
MCLAURIN_ATN_APPROX
MCLAURIN_ATN_SIMPLE
MCLAURIN_BI_LE
MCLAURIN_COS
MCLAURIN_EXP_LE
MCLAURIN_EXP_LE1
MCLAURIN_EXP_LEMMA
MCLAURIN_EXP_LT
MCLAURIN_LN_NEG
MCLAURIN_LN_POS
MCLAURIN_NEG
MCLAURIN_SIN
MCLAURIN_ZERO
MDIFF
MDIST_CONGRUENT_TRIPLES_0
MDIST_EQ_0
MDIST_EQ_ORIGIN
MDIST_INCREASES_ONLINE
MDIST_KLEINIFY
MDIST_KLEINIFY_EQ
MDIST_KLEINIFY_MOEBIUS
MDIST_POS_LE
MDIST_POS_LT
MDIST_REFL
MDIST_SYM
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_LIFT_RPOW
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
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_CONVEX_HULL_2_TRIVIAL
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_LE
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_SUMS_COMPACT_EPSILON
MEASURE_TETRAHEDRON
MEASURE_TRANSLATION
MEASURE_TRIANGLE
MEASURE_UNION
MEASURE_UNIONS_LE
MEASURE_UNIONS_LE_IMAGE
MEASURE_UNION_LE
MEASURE_UNIQUE
MEM
MEMBER
MEMBERS_ISASET
MEMBER_NOT_EMPTY
MEMPTY
MEM_APPEND
MEM_APPEND_DECOMPOSE
MEM_APPEND_DECOMPOSE_LEFT
MEM_ASSOC
MEM_COUNT
MEM_DELETE1
MEM_DELETE1_MEM_IMP
MEM_EL
MEM_EXISTS_EL
MEM_FILTER
MEM_LINEAR_IMAGE
MEM_LIST_OF_SET
MEM_MAP
MEM_MAXL
MEM_PERMUTATION
MEM_QSORT
MEM_REMOVE
MEM_REVPERM
MEM_TRANSLATION
MERTENS
MERTENS_LEMMA
MERTENS_LIMIT
MERTENS_MANGOLDT_VERSUS_LOG
MESSY_JESSE2
METRIC_BOUND_LEMMA
METRIC_ISMET
METRIC_NZ
METRIC_POS
METRIC_SAME
METRIC_SYM
METRIC_TRIANGLE
METRIC_ZERO
MEXTENSION
MIDPOINT
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
MIN
MINIMAL
MINIMAL_IN_INSERT
MINKOWSKI
MINKOWSKI_COMPACT
MINL
MINUSINF_LEMMA
MINUSINF_MIRROR
MINUSINF_REPEATS
MIN_GT
MK_COMB_correct
MK_REC_INJ
MK_V_CLAUSES
MK_V_SET
MMEMBER_MDIFF
MMEMBER_MSING
MMEMBER_MUNION
MOBIUS_0
MOBIUS_1
MOBIUS_INVERSION
MOBIUS_MULT
MOBIUS_PRIME
MOBIUS_PRIMEPOW
MODAL_REFL
MODAL_SERIAL
MODAL_SYM
MODAL_TRANS
MODAL_WFTRANS
MOD_ADD_MOD
MOD_EQ
MOD_EQ_0
MOD_EXISTS
MOD_EXP_MOD
MOD_LE
MOD_LT
MOD_MOD
MOD_MOD_EXP_MIN
MOD_MOD_REFL
MOD_MULT2
MOD_MULT_ADD
MOD_MULT_CONG
MOD_MULT_LMOD
MOD_MULT_MOD2
MOD_MULT_RMOD
MOD_NSUM_MOD
MOD_NSUM_MOD_NUMSEG
MOD_UNIQ
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_AC
MONOIDAL_ADD
MONOIDAL_AND
MONOIDAL_COMPLEX_MUL
MONOIDAL_INT_ADD
MONOIDAL_LIFTED
MONOIDAL_MATRIX_ADD
MONOIDAL_MUL
MONOIDAL_POLY_ADD
MONOIDAL_REAL_ADD
MONOIDAL_REAL_MUL
MONOIDAL_SUMSET
MONOIDAL_VECTOR_ADD
MONOTONE_BIGGER
MONOTONE_CONVERGENCE_DECREASING
MONOTONE_CONVERGENCE_INCREASING
MONOTONE_CONVERGENCE_INTERVAL
MONOTONE_SUBSEQUENCE
MONOTONIC_ASSERT
MONOTONIC_ASSIGN
MONOTONIC_IF
MONOTONIC_ITE
MONOTONIC_SEQ
MONOTONIC_VARIANT
MONOTONIC_WHILE
MONO_ALL
MONO_ALL2
MONO_COND
MONO_EXISTS
MONO_FORALL
MONO_ON_SUBSET
MONO_SUC
MONTEL
MORDER_WF
MORERA_LOCAL_TRIANGLE
MORERA_LOCAL_TRIANGLE_GEN
MORERA_TRIANGLE
MORLEY
MOVE_INVARIANT
MPOW_1
MPOW_ADD
MPOW_SUC
MR1_ADD
MR1_ADD_LE
MR1_ADD_LT
MR1_BETWEEN1
MR1_BOUNDED
MR1_DEF
MR1_LIMPT
MR1_SUB
MR1_SUB_LE
MR1_SUB_LT
MSING
MSUM_ADD
MSUM_CLAUSES
MSUM_CLAUSES_LEFT
MSUM_CLAUSES_NUMSEG
MSUM_CMUL
MSUM_COMPONENT
MSUM_EQ
MSUM_IMAGE
MSUM_MATRIX_LMUL
MSUM_MATRIX_RMUL
MSUM_NEG
MSUM_OFFSET
MSUM_RESTRICT_SET
MSUM_SING
MSUM_SUB
MSUM_SUPPORT
MTOP_LIMPT
MTOP_OPEN
MTOP_TENDS
MTOP_TENDS_UNIQ
MUA_DIV_CONST
MUA_MUA
MUA_MUB
MUB_DIV_CONST
MUB_MUA
MUB_MUB
MULT
MULTA
MULTA0
MULTA_S
MULTIPLE_COUNTING_LEMMA
MULTIPLICATIVE
MULTIPLICATIVE_1
MULTIPLICATIVE_CONST
MULTIPLICATIVE_CONVOLUTION
MULTIPLICATIVE_DELTA
MULTIPLICATIVE_DIVISORSUM
MULTIPLICATIVE_GCD
MULTIPLICATIVE_ID
MULTIPLICATIVE_IGNOREZERO
MULTIPLICATIVE_PHI
MULTIPLICATIVE_POWERSUM
MULTIPLICATIVE_SIGMA
MULTIPLICATIVE_TAU
MULTIPLICATIVE_UNIQUE
MULTIPLICITY_MULTISET
MULTIPLICITY_OTHER_ROOT
MULTIPLICITY_UNIQUE
MULTIPLICITY_WORKS
MULTISET_INDUCT
MULTISET_INDUCT_LEMMA1
MULTISET_INDUCT_LEMMA2
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
MULT_0
MULT_2
MULT_AC
MULT_ASSOC
MULT_CLAUSES
MULT_DIV_2
MULT_DIV_LE
MULT_EQ_0
MULT_EQ_1
MULT_EQ_COPRIME
MULT_EXP
MULT_FIX
MULT_LCANCEL
MULT_MONO_EQ
MULT_NSUM
MULT_SUC
MULT_SYM
MUL_C_UNIV
MUNION
MUNION_11
MUNION_AC
MUNION_ASSOC
MUNION_EMPTY
MUNION_INUNION
MUNION_MEMPTY
MUTEX
MU_DIV_CONST
MU_PROD
MVT
MVT2
MVT_ALT
MVT_GENERAL
MVT_INEQ
MVT_LEMMA
MVT_SIMPLE
MVT_VERY_SIMPLE
main_lem000
main_lem001
main_lem002
mangoldt
mark_term
mat
matinsert_lem0
matrix
matrix_add
matrix_cmul
matrix_inv
matrix_mul
matrix_neg
matrix_sub
matrix_vector_mul
max_num_sequence
max_real
max_real_le
max_real_symm
mbasis
mdiff
mdist
measurable
measurable_on
measure
meeting_lemma
memma
mempty
metric_cont
metric_continuous_continuous
metric_continuous_continuous_top2
metric_continuous_domain
metric_continuous_pt_domain
metric_continuous_range
metric_euclid
metric_euclidean
metric_hausdorff
metric_real
metric_space_symm
metric_space_triangle
metric_space_zero
metric_space_zero2
metric_subspace
metric_translate
metric_translate_LEFT
mid_end_disj
midpoint
midpoint_edge
midpoint_exclusion
midpoint_exists
midpoint_h_edge
midpoint_unique
midpoint_v_edge
min_finite
min_finite_delta
min_least
min_num
min_real
min_real_le
min_real_symm
minimal
minusinf
mirror
mk_line_2
mk_line_fin_inter
mk_line_hyper2_e1
mk_line_hyper2_e2
mk_line_hyper2_fst
mk_line_hyper2_snd
mk_line_inter
mk_line_pt
mk_line_sub
mk_line_symm
mk_pair_def
mk_segment_convex
mk_segment_end
mk_segment_endpoint
mk_segment_eq
mk_segment_h
mk_segment_hc
mk_segment_hyperplane
mk_segment_image
mk_segment_inj_image
mk_segment_inj_image2
mk_segment_simple_arc_end
mk_segment_sym
mk_segment_sym_lemma
mk_segment_v
mk_segment_vc
mmember
mobius
modusponens
moebius_function
monic_isign_lem
mono
mono_dec
mono_inc
mono_inc_dec
mono_inc_pow
mono_inc_pow_const
mono_on
mono_unbounded
mono_unbounded_above
mono_unbounded_above_pos
mono_unbounded_below
mono_unbounded_below_neg
monoidal
monotonic
morder
move
move2Cond
moveInvariant
moveSymmetry
mpow
mr1
msing
msum
mtop
mtop_istopology
mua_neg
mua_neg2
mua_quotient_limit
mua_quotient_limit_neg
mub_quotient_limit
mul_c
mul_odd_lem
multiplicative
multiplicity
multiset_tybij_th
multivec
multivector
multivector_tybij_th
munion
mutex