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)
mark_termmax_num_sequence
max_real
max_real_le
max_real_symm
meeting_lemma
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_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
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_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