HOL html

Files Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _
Theorems Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _

M (theorems)

MAEWNPU
MAP_AB_EMPTY
MAP_EDGES_FACET_INTO_E1_FAN
MAP_EDGES_FACET_INTO_E1_FAN_INJ
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_FULL_LINEAR_EQUATIONS
MATRIX_I
MATRIX_ID
MATRIX_INV
MATRIX_INVERTIBLE
MATRIX_INV_COFACTOR
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_LTRANSP_DOT_COLUMN
MATRIX_MUL_LZERO
MATRIX_MUL_RID
MATRIX_MUL_RIGHT_COFACTOR
MATRIX_MUL_RINV
MATRIX_MUL_RMUL
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_SUB
MATRIX_NONFULL_LINEAR_EQUATIONS
MATRIX_NONFULL_LINEAR_EQUATIONS_EQ
MATRIX_OF_MATRIX_VECTOR_MUL
MATRIX_RIGHT_INVERSE_COFACTOR
MATRIX_RIGHT_INVERTIBLE
MATRIX_RIGHT_INVERTIBLE_INDEPENDENT_ROWS
MATRIX_RIGHT_INVERTIBLE_SPAN_COLUMNS
MATRIX_RIGHT_INVERTIBLE_SURJECTIVE
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_WORKS
MATVEC_ADD
MATVEC_SUB
MATVEC_VECMATS_ID
MAT_COMPONENT
MAXIMAL_INDEPENDENT_SUBSET
MAXIMAL_INDEPENDENT_SUBSET_EXTEND
MAX_COPLANAR_4POINT
MAX_IF_COPLANAR
MAX_IF_COPLANAR1
MAX_REAL3_LESS_EX
MAX_REAL_LESS_EX
MCELL0
MCELL1
MCELL1_EXPLICIT
MCELL1_RADIAL
MCELL1_SOL_RESTRICT
MCELL1_VOL
MCELL1_VOL_RESTRICT
MCELL2
MCELL2_CELL_PARAMETERS_EXIST
MCELL2_CONVEX
MCELL2_CRITICAL_WEIGHT1
MCELL2_DIHV_AZIM
MCELL2_DIHV_LT_PI
MCELL2_DIHX
MCELL2_DIHX_POS
MCELL2_EDGE
MCELL2_EDGE_FIRST
MCELL2_HL_LT_SQRT2
MCELL2_INTER_BIS_LE_MEASURABLE
MCELL2_PARAM_D_UL
MCELL2_PARAM_UL
MCELL2_PERMUTE_01
MCELL2_SOL
MCELL2_SPLIT
MCELL2_SUBSET_AFF_GE
MCELL2_VERTEX
MCELL2_VOL
MCELL2_VOL_SPLIT
MCELL2_VOL_SPLIT_EXPLICIT
MCELL2_VX_PROPS
MCELL3
MCELL3_008
MCELL3_CELL_PARAMETERS_EXIST
MCELL3_CONVEX_HULL
MCELL3_CRITICAL_WEIGHT
MCELL3_DIHX
MCELL3_DIHX_POS
MCELL3_DOMAIN
MCELL3_EDGE
MCELL3_EDGE_EXPLICIT
MCELL3_EDGE_FIRST
MCELL3_EXTREME_CARD
MCELL3_NONPLANAR
MCELL3_PARAM_UL
MCELL3_SET_OF_LIST_VX
MCELL3_VX
MCELL4
MCELL4_AZIM_LT_PI
MCELL4_BARV_FI
MCELL4_CARD4
MCELL4_CELL_PARAMETERS_EXIST
MCELL4_CONVEX_HULL
MCELL4_DIHX_AZIM
MCELL4_DOMAIN
MCELL4_EDGE
MCELL4_EDGE_EXPLICIT
MCELL4_EDGE_FIRST
MCELL4_EDGE_OPP
MCELL4_EXTREME_POINT
MCELL4_FI
MCELL4_FI_EL
MCELL4_FULL_WEDGE
MCELL4_GG
MCELL4_LEAF2
MCELL4_LEAF3
MCELL4_LEAF_S_LEAF
MCELL4_NONPLANAR
MCELL4_PARAM_UL
MCELL4_REPARAM
MCELL4_SET_OF_LIST_VX
MCELL4_VX
MCELL_2_PROPERTIES_lemma1
MCELL_ARG_REDUCE
MCELL_AVOID_LEAVES
MCELL_BUMP_0
MCELL_BUMP_OPP
MCELL_CELL_PARAMETERS_D_EXIST
MCELL_CELL_PARAMETERS_EXIST
MCELL_CONVEX
MCELL_EDGE
MCELL_EDGE_FIRST
MCELL_EXPLICIT
MCELL_EXTREME_DIFF_V
MCELL_ID_MXI
MCELL_ID_MXI_2
MCELL_ID_OMEGA_LIST_N
MCELL_IN_WEDGE
MCELL_PARAM_D_UL
MCELL_PARAM_UL
MCELL_SET_NOT_EMPTY
MCELL_SUBSET_BALL8
MCELL_SUBSET_BALL8_1
MCELL_SUBSET_BALL8_2
MCELL_SUBSET_BALL_4
MCELL_V_INTER_EXTREME
MCELL_WEDGE_UNIQUE
MEASURABLE_AFF_3_UNION_INTER_BALL
MEASURABLE_AFF_GT_2_1_INTER_BALL
MEASURABLE_BALL_AFF_GE
MEASURABLE_BALL_INTER_UNIV
MEASURABLE_CONIC_CAP_WEDGE_GE
MEASURABLE_MCELL
MEASURABLE_ROGERS
MEASURABLE_TOPOLOGICAL_COMPONENT_YFAN_INTER_BALL
MEASURABLE_UNIONS
MEASURABLE_UNIONS2
MEASURABLE_VORONOI_CLOSED
MEASURE_AFF_3
MEASURE_AFF_3_FAN
MEASURE_AFF_3_INTER_BALL
MEASURE_AFF_3_UNION_FAN
MEASURE_AFF_GT_2_1
MEASURE_AFF_GT_2_1_INTER_BALL
MEASURE_VORONOI_CLOSED_OPEN
MEASURE_XFAN
MEASURE_XFAN_INTER_BALL
MEASURE_YFAN_INTER_BALL
MEETING_CONDITION
MEM_A_EMPTY
MEM_FACE_LEMMA
MEM_FIND_FACE
MEM_FIND_FACE_IMP_FACES_EQ
MEM_FIND_FACE_IMP_MEM_DARTS
MEM_FIND_FACE_NONEMPTY
MEM_FIND_LIST
MEM_FIND_LIST_NONEMPTY
MEM_FIND_PAIR_LIST
MEM_FLATTEN
MEM_F_LIST
MEM_IMP_NOT_ALL_DISTINCT_APPEND
MEM_LEFT_ACTION_LIST
MEM_LEFT_ACTION_LIST_2
MEM_LEFT_ACTION_LIST_3
MEM_LINEAR_IMAGE
MEM_LIST_OF_DARTS
MEM_LIST_OF_ELEMENTS
MEM_LIST_PAIRS
MEM_LIST_PAIRS_EXISTS
MEM_LIST_PAIRS_EXPLICIT
MEM_NEXT_EL
MEM_NUM_EMPTY
MEM_NUM_PAIR_EMPTY
MEM_PREV_EL
MEM_REMOVE_DUPLICATES
MEM_SHIFT_LEFT
MEM_SHIFT_RIGHT
MEM_TRANSLATION
MEM_ZIP
MESURABLE_YFAN_INTER_BALL
MET_LAM_ROI
MFKLVDK
MHAEYJN
MHAEYJN_CONVEX_LOCAL_FAN
MHFTTZN1
MHFTTZN2
MHFTTZN3
MHFTTZN4
MHFTTZN_lemma
MHFTTZN_lemma2
MIDDLE_POINT
MIDDLE_POINT_IN_CONV2
MIDPOINT_COLLINEAR
MIDPOINT_EQ_ENDPOINT
MIDPOINT_IN_CONV0
MIDPOINT_LINEAR_IMAGE
MIDPOINT_REFL
MIDPOINT_SYM
MID_COND
MID_POINT_EXISTS
MINIMAL_INTERS_EXISTS
MINIMAL_INTER_INTERS_EXISTS
MINIMAL_QUADRATIC_POLY
MINIMIZE_OVER_2
MINIMIZE_OVER_MEMBERS
MINIMIZE_OVER_STRONGER
MINIMUM_IN_B_SY
MIN_LEAST
MIN_NOT_STAND_4M7
MIN_NOT_STAND_4M8
MIN_NUM_LE_IMAGE
MIN_NUM_SUBSET
MIQMCSN
MIXED_PROD_POS_IMP_RANGE_AZIM
MK_CELL_DOMAIN
MK_PLANAR_REP
MK_PLANAR_V3_DEFOR_V1
MK_PLANAR_V3_DEFOR_V1_FUN
MK_PLANAR_V3_DEFOR_V2_FUN
MK_SIMPLEX_TRANSLATION
MMS_IMP_BBPRIME
MMS_IMP_BBPRIME2
MMS_IMP_BBS
MM_3M1_prime_IMP_MM_3M1
MM_3T1_prime_IMP_MM_3T1
MM_3T3_prime_IMP_MM_3T3
MM_3T4_prime2_IMP_MM_3T4
MM_3T4_prime_IMP_MM_3T4
MM_4I1_IMP_STAB_4I1
MM_4I2_IMP_4T2_4T1
MM_4I3_IMP_4M6
MM_4I3_IMP_4T4
MM_4I3_IMP_STAB_4I3
MM_4M2_IMP_4M6
MM_4M2_IMP_STAB_4M2
MM_4M3_IMP_4M6
MM_4M3_IMP_STAB_4M3
MM_4M4_IMP_4M7
MM_4M4_IMP_STAB_4M4
MM_4M5_IMP_4M8
MM_4M5_IMP_STAB_4M5
MM_4M6_IMP_4T5
MM_4M6_IMP_MM_4T3
MM_4M6_IMP_STAB_4M6
MM_4M6_prime_IMP_MM_4M6
MM_4M7_IMP_MM_4M6_01
MM_4M7_IMP_MM_4M6_12
MM_4M7_IMP_STAB_4M7
MM_4M7_prime_IMP_MM_4M7
MM_4M8_IMP_MM_4M6_01
MM_4M8_IMP_MM_4M6_23
MM_4M8_IMP_MM_4M8_02
MM_4M8_IMP_MM_4M8_13
MM_4M8_IMP_STAB_4M8
MM_4M8_prime_IMP_MM_4M8
MM_5I1_IMP_MM_5M2
MM_5I2_IMP_MM_5M2
MM_5I3_IMP_MM_5M1
MM_5I3_IMP_MM_5M2
MM_5M1_IMP_MM_5M2
MM_5M2_IMP_MM_STAB_5I2
MM_5M2_IMP_MM_STAB_5I3
MM_5M2_IMP_MM_STAB_5M2
MM_5M2_IMP_MM_STAB_5M3
MM_IS_NOT_1EMPTY_SUBDIVISION
MM_IS_NOT_1EMPTY_SUBDIVISION1
MM_IS_NOT_2EMPTY_SUBDIVISION
MM_IS_NOT_2EMPTY_SUBDIVISION1
MM_IS_NOT_2EMPTY_SUBDIVISION_C_EQ_AM
MM_SCS_OPP
MMs_minimize_tau_fun
MMs_v39
MOD_4_CASES
MOD_4_EXPLICIT
MOD_5_EXPLICIT
MOD_ADD_125
MOD_ADD_135
MOD_ADD_215
MOD_ADD_225
MOD_ADD_235
MOD_ADD_245
MOD_ADD_315
MOD_ADD_325
MOD_ADD_335
MOD_ADD_345
MOD_ADD_425
MOD_ADD_435
MOD_ADD_SUB_1
MOD_EQ_IMP_MOD_EQ_0
MOD_EQ_MOD
MOD_EQ_MOD1
MOD_EQ_MOD_SHIFT
MOD_IMP_EQ
MOD_INJ
MOD_INJ1
MOD_INJ1_ALT
MOD_IN_NUMSEG
MOD_NUMSEG
MOD_PERIODIC
MOD_PERIOD_BOUNDED
MOD_PERIOD_BOUNDED2
MOD_PERIOD_BOUNDED_ALT
MOD_REFL
MOD_SHIFT
MOD_SUC_MOD
MOD_SURJ
MOD_periodic2
MONG7_ROI
MONOIDAL_VECTOR_ADD
MONOPOLY_IN_FIRST_PERIOD
MONOTONE_BIGGER_FAN
MONOTONE_SUBSEQUENCE_FAN
MONO_AZIM_AS_BTA_I
MONO_AZIM_POWER_SIGMA_FAN
MONO_AZIM_SIGMA_FAN
MONO_E_FAN
MONO_F1_FAN
MONO_LE_IN_FIRST_PERIOD
MONO_N_FAN
MONO_POWER_MAP_POINTS1_FAN
MONO_POWER_SIGMA_FAN
MONO_SIGMA_FAN
MOST_EXPAND_IN_WEDGE_GE
MOVE_NORM_OUT_OF_SQRT
MOVE_TO_UNIT_INTERVAL
MOZNWEH
MTMLSRF
MULT_INVERSE_POWER
MUL_0_n
MUL_B0_t
MUL_BIT0_t
MUL_NUM
MUL_SUC_RIGHT
MUL_n_0
MXHKOXR
MXI_BETWEEN
MXI_EXPLICIT
MXI_EXPLICIT_OLD
MXI_IN_VORONOI_LIST
MXI_NOT_IN_V
MXQTIED
MXQTIED_BB
MXQTIED_INDEX
MXQTIED_PRIME
MXQTIED_PRIME2
MXQTIED_TAU
MXQTIED_TAU_DSV
MYOQCBS
M_CELL_CONVEX_PASS_LEMMA
M_CELL_DECREASING_PASS_LEMMA
M_CELL_INCREASING_PASS_LEMMA
M_CELL_LIST_PASS1_LEMMA
M_CELL_LIST_PASS_GLUE_LEMMA
M_CELL_PASS_EQ_LIST_PASS1
M_CELL_PASS_GLUE_LEMMA
M_CELL_PASS_IMP_LIST_PASS1
M_CELL_PASS_LEMMA
M_CELL_SUP
M_RESTRICT_LEFT_LEMMA
M_RESTRICT_RIGHT_LEMMA
M_TAYLOR_BOUND'
M_TAYLOR_ERROR_ITLIST2
M_TAYLOR_ERROR_ITLIST2_ALT
M_TAYLOR_ERROR_LIST_SUM2
M_TAYLOR_LOWER_BOUND'
M_TAYLOR_LOWER_PARTIAL_BOUND'
M_TAYLOR_PARTIAL_BOUND'
M_TAYLOR_PARTIAL_LOWER'
M_TAYLOR_PARTIAL_UPPER'
M_TAYLOR_UPPER_BOUND'
M_TAYLOR_UPPER_PARTIAL_BOUND'
m1_minus_12m2
m_bounded_on_int
m_cell_domain
m_cell_list_pass
m_cell_pass
m_lin_approx
m_taylor_error
m_taylor_interval
m_taylor_partial_error
machine_eps
main_lemma
make_point
map
map1
map3
map3_define
mapAt1
map_permutes_outside_domain
map_to_ball
map_to_nua_kg
map_to_voronoi
marchal
marchal_minus_lfun
marchal_quartic
marchal_quartic_continuous_at
mardih2_x
mardih3_x
mardih4_x
mardih5_x
mardih6_x
mardih_x
margin_in_loop
margin_in_support_darts
mark_term
mask
mat
matan
matan_pos
matrix
matrix_add
matrix_cmul
matrix_inv
matrix_mul
matrix_neg
matrix_sub
matrix_vector_mul
matvec
max_num_sequence
max_real
max_real3
max_real_symm
maxn
mcell
mcell0
mcell1
mcell2
mcell3
mcell3_dihX_dih_y
mcell3_dihXb_dih_y
mcell3_gammaX_gamma3f
mcell3_gammaXb_gamma3f
mcell4
mcell4_convex_hull
mcell_set
mcell_set_2
mcell_set_alt
mdtau2_fake
mdtau2uf_y
mdtau2uf_y_LC
mdtau_fake
mdtau_y
mdtau_y_LC
mea_unions_ccube_le_card
measurable_ccube
measurable_cube
measurable_dartset_leads_into30_fan
measurable_dartset_leads_into3_fan
measurable_normball
measurable_normball0
measurable_packing_lm1
measurable_packing_lm2
measurable_unions_ccube
measurable_unions_cube
measurable_unions_voronoi
measurable_voronoi
measure_ball_diff_set_negligible
measure_ccube
measure_cube
measure_element_set_ccube
measure_hinhcau
measure_ineq_lm53_1
measure_ineq_lm53_2
measure_unions_cube_less_ball
measure_unions_of_cube
measure_unions_sum_voronoi
merge_sort
midpoint
min_dist
min_dist_k
min_exp_def
min_k
min_least
min_list
min_list_liz
min_num
min_num_in
min_num_insert
min_num_le
min_num_single
min_num_unique
min_polar
min_real
minconvex3
minimal_fan
minimally_nonconforming_fan
minn
minn_MIN
mirror
mk_126
mk_135
mk_456
mk_planar2
mk_planar2_continuous
mk_planar_unique
mk_simplex1
mk_simplex_uniq
mk_unadorned_v39
mk_vec3
mkseq
mm1
mm2
mod_plus
module_of_vector
mono_cyclic_power_sigma_fan
monomial
morphism
mu6_x
mu6_x_mu_y
muR
muR_ALT
muRa
mu_y
mu_y_ft_combine
mu_y_ft_combine2
mu_y_sym
mu_y_sym_cases
mudL_234_x
mudLs_126_x
mudLs_135_x
mudLs_234_x
mud_126_135
mud_126_x
mud_135_x
mud_234_x
mudd_126_x_v2
mudd_135_x_v2
mudt_234_x
mul6
mul_nn
mul_nocancel
mul_partial_lemma'
mul_pp
mul_second_lemma'
multiplication_exponents
muy_delta
muy_v
mxi
my_assum
my_thm