HOL html

Files Index

Theorems Index

S (theorems)

SELECT_EXIST
SELECT_THM
SER_APPROX
SER_APPROX1
SKOLEM_TAG
SKOLEM_TAG2
SUBSET_INTER
SUBSET_INTERS
SUBSET_PREIMAGE
SUBSET_SUC
SUBSET_SUC2
SUBSET_UNIONS_INSERT
SUB_IMP_INTER
SUPP
SURJ_FINITE
SURJ_IMAGE
SWAP_EXISTS_THM
SWAP_FORALL_TAG
segment_delete
segment_end_cls
segment_end_cls2
segment_end_disj
segment_end_finite
segment_end_inj
segment_end_select
segment_end_sing
segment_end_symm
segment_end_trans
segment_end_union
segment_end_union_lemma
segment_end_union_rectagon
segment_euclid
segment_finite
segment_in_comp
segment_not_in
segment_of_G
segment_of_endpoint
segment_of_eq
segment_of_finite
segment_of_in
segment_of_segment
segment_of_subset
segment_superset_endpoint
segment_union
segment_union2
segpath_end
segpath_inj
segpath_lemma
segpathxy
select_card_max
select_card_min
select_image_num_max
select_image_num_min
select_num_max
sequence_in
sequence_subseq
set_dist_eq
set_dist_inf
set_dist_nn
set_dist_pos
set_lower_delete
set_lower_n
shift_inj
simple_arc_ball_cover
simple_arc_ball_cover_ver2
simple_arc_choose_end
simple_arc_compact
simple_arc_conn_complement
simple_arc_connected
simple_arc_constants
simple_arc_coord
simple_arc_end_IVT
simple_arc_end_closed
simple_arc_end_cont
simple_arc_end_cut
simple_arc_end_distinct
simple_arc_end_edge_closure
simple_arc_end_edge_full_closure
simple_arc_end_end
simple_arc_end_end2
simple_arc_end_end_closed
simple_arc_end_end_closed2
simple_arc_end_homeo
simple_arc_end_inj
simple_arc_end_plane_select
simple_arc_end_restriction
simple_arc_end_select
simple_arc_end_simple
simple_arc_end_subset_trans
simple_arc_end_subset_trans_lemma
simple_arc_end_symm
simple_arc_end_trans
simple_arc_euclid
simple_arc_finite_lemma1
simple_arc_finite_lemma2
simple_arc_finite_lemma3
simple_arc_finite_lemma4
simple_arc_finite_pointI
simple_arc_grid_properties
simple_arc_homeo
simple_arc_infinite
simple_arc_midpoint
simple_arc_nonempty
simple_arc_segment
simple_arc_sep
simple_arc_sep2
simple_arc_sep3
simple_arc_sep_three_t
simple_arc_uniformly_continuous
simple_closed_curve_2pt
simple_closed_curve_closed
simple_closed_curve_compact
simple_closed_curve_cut_unique
simple_closed_curve_cut_unique_inter
simple_closed_curve_euclid
simple_closed_curve_mk_ABD
simple_closed_curve_mk_C
simple_closed_curve_mk_E
simple_closed_curve_nonempty
simple_closed_curve_nsubset_arc
simple_closed_curve_pt
simple_closed_cut
sin_half
sin_period
sin_period_int
sin_period_neg
sing_has_size1
single_inter
single_subset
sinx_le_x
sqrt_frac
squ_closure
squ_closure_down_h
squ_closure_h
squ_closure_hc
squ_closure_left_v
squ_closure_right_v
squ_closure_up_h
squ_closure_up_hc
squ_closure_v
squ_closure_vc
squ_disj
squ_down
squ_euclid
squ_induct
squ_inj
squ_inter
squ_left_even
squ_left_odd
squ_left_par
squ_squc
squ_squc_C
squ_subset_sqc
square_cell
square_col
square_disj
square_domain
square_floor0
square_floor1
square_h_edge
square_h_edgeV2
square_le
square_pointI
square_pointIv2
square_row
square_square
square_v_edge
square_v_edgeV2
squc_closed
squc_h
squc_inter
squc_lemma4
squc_union
squc_union_lemma1
squc_union_lemma2
squc_union_lemma3
squc_v
ssqrt
star_avoidance
star_avoidance_contrp
star_avoidance_lemma1
strict_dom_irrefl
strict_dom_trans
strict_lemma
strip_le_lemma
strip_lt_lemma
sub_union
subf_cont
subf_lemma
subs_lemma
subseq_cauchy
subsequence_rec
subset3_absorb
subset_antisym_eq
subset_cauchy
subset_closure
subset_contain
subset_imp
subset_imp_eq
subset_inter_pair
subset_of_closure
subset_preimage
subset_sequence
subset_union_inter
subset_union_pair
suc_div
suc_interval
suc_sum
sum_vector
sum_vector_EXISTS
supm_UB
supm_eps
supm_unique
supp
switch_lemma_le
switch_lemma_let
switch_lemma_lt
symmetric