HOL html

Files Index

Theorems Index

C (theorems)

CARD_DELETE_CHOICE
CARD_GE_REFL
CARD_SING
CARD_SING_CONV
CARD_SUC_DELETE
COMP_ASSOC
COMP_BIJ
COMP_INJ
COMP_SURJ
COUNTABLE_CARD
COUNTABLE_IMAGE
COUNTABLE_NUMSEG
COUNTABLE_UNIONS
c_edge_euclid
card_gt_3
card_has_subset
card_inj
card_sing
card_subset_lt
card_suc_insert
card_surj_bij
cartesian_el
cartesian_finite
cartesian_pair
cartesian_size
cartesian_univ
cases4
cauchy_schwartz
cauchy_seq_cauchy
cauchy_subseq
cauchy_subseq_sublemma
cell_clauses
cell_convex
cell_euclid
cell_inter
cell_mem
cell_nonempty
cell_partition
cell_rules
cell_unions
cell_unions_disj
cell_ununion
center_FINITE
cis0
cis3pi2
cis_distinct
cis_exist_lemma
cis_inj
cis_lemma
cis_nz
cispi
cispi2
closed_UNIV
closed_ball2_center
closed_ball_closed
closed_ball_compact
closed_ball_empty
closed_ball_inter
closed_ball_pt
closed_ball_subset_larger_open
closed_ball_subset_open
closed_compact
closed_half_plane2D_FLE
closed_half_plane2D_FLT_closed
closed_half_plane2D_FLT_convex
closed_half_plane2D_LEF
closed_half_plane2D_LES
closed_half_plane2D_LTF_closed
closed_half_plane2D_LTF_convex
closed_half_plane2D_LTS_closed
closed_half_plane2D_LTS_convex
closed_half_plane2D_SLE
closed_half_plane2D_SLT_closed
closed_half_plane2D_SLT_convex
closed_half_space_closed
closed_half_space_convex
closed_half_space_diff
closed_half_space_euclid
closed_half_space_inter
closed_half_space_scale
closed_inter
closed_inter2
closed_open
closed_point
closed_union
closedball_convex
closedball_mk_segment_end
closure_FLT
closure_LTF
closure_LTS
closure_SLT
closure_close
closure_closed
closure_empty
closure_euclid
closure_half_space
closure_imp_adj
closure_inter
closure_open
closure_open_ball
closure_open_interval
closure_real_set
closure_segment
closure_self
closure_subset
closure_union
closure_unions
closure_univ
cls_edge
cls_edge_size2
cls_empty
cls_h
cls_inj
cls_inj_lemma_h
cls_inj_lemma_hv
cls_inj_lemma_v
cls_subset
cls_union
cls_v
col_disj
comp_comp
comp_h_rect
comp_h_squ
comp_p_squ
comp_pointI_long
comp_squ
comp_squ_adj
comp_squ_down_rect
comp_squ_down_rect_h
comp_squ_fill
comp_squ_left_rect
comp_squ_left_rect_v
comp_squ_right_left
comp_squ_right_rect
comp_squ_right_rect_v
comp_squ_up_rect
comp_squ_up_rect_h
comp_v_rect
comp_v_squ
compact_closed
compact_complete
compact_distance
compact_euclid
compact_inf
compact_infm
compact_max
compact_max_real
compact_min_real
compact_point
compact_subset
compact_sup
compact_supm
compact_totally_bounded
compact_uniformly_continuous
complete_closed
complete_compact
complete_euclid
complete_real
component
component_empty
component_homeo
component_imp_connected
component_properties
component_refl
component_reflA
component_reflB
component_reflC
component_replace
component_simple_arc
component_simple_arc_ver2
component_symm
component_trans
component_unions
compose
compose_cont
compose_image
conn2_cls3
conn2_has_rectagon
conn2_imp_conn
conn2_no1
conn2_proper
conn2_psegment_triple
conn2_rect_diff_inner
conn2_rectagon
conn2_sequence
conn2_sequence_lemma1
conn2_sequence_lemma2
conn2_sequence_lemma3
conn2_sequence_lemma4
conn2_sequence_lemma5
conn2_union
conn2_union_edge
conn_splice
conn_union
connect_image
connect_real
connect_real_open
connected_component
connected_empty
connected_homeo
connected_in_edge
connected_induced
connected_induced2
connected_metric
connected_metric_pair
connected_mk_segment
connected_nogap
connected_open
connected_open_closure
connected_sing
connected_unions
connected_unions_common
const_continuous
construct_hv_finite
cont_domain
cont_extend_real_lemma
cont_mk_segment
continuous_I
continuous_comp
continuous_delta
continuous_euclid1
continuous_induced
continuous_induced_domain
continuous_interval
continuous_lin_combo
continuous_metric_extend
continuous_neg_delta
continuous_range
continuous_real_const
continuous_real_mul
continuous_scale
continuous_sum
continuous_uninduced
converge_cauchy
convergent_subseq
convex_component
convex_component_ver2
convex_connected
convex_connected_ver2
convex_inter
convex_pointI
coord01
coord_dirac
cos_double2
cos_period
cos_period_int
cos_period_neg
cos_sin_reduce
cosdiff2
count_iso_scale
count_iso_translate
countable_cover
countable_dense
countable_prod
ctop_comp_open
ctop_open
ctop_reflA
ctop_reflB
ctop_reflC
ctop_top
ctop_top2
ctop_top2_ver2
ctop_unions
curve_annulus_lemma
curve_cell_cell
curve_cell_cls
curve_cell_edge
curve_cell_empty
curve_cell_finite_union
curve_cell_grid_unions
curve_cell_h
curve_cell_h_inter
curve_cell_h_inter_ver2
curve_cell_h_ver2
curve_cell_imp_subset
curve_cell_in
curve_cell_not_point
curve_cell_not_point_ver2
curve_cell_point
curve_cell_sing
curve_cell_squ
curve_cell_squ_inter
curve_cell_squ_inter_ver2
curve_cell_squ_ver2
curve_cell_subset
curve_cell_union
curve_cell_v
curve_cell_v_inter
curve_cell_v_inter_ver2
curve_cell_v_ver2
curve_circle_lemma
curve_closed
curve_closed_ver2
curve_closure
curve_closure_ver2
curve_point_unions
curve_point_unions_ver2
curve_restriction
curve_simple_lemma
cut_arc_inter
cut_arc_inter_lemma
cut_arc_order
cut_arc_replace
cut_arc_simple
cut_arc_simple2
cut_arc_subset
cut_arc_symm
cut_arc_unique
cut_psegment
cut_rectagon
cut_rectagon_cls
cut_rectagon_unique