HOL html

Files Index

Theorems Index

L (theorems)

L
L13_LEMMA
LAMBDA_BETA_3
LAMBDA_BETA_PERM
LAMBDA_TRIPLED_THM
LDURDPN
LEAF_BARV
LEAF_DOMAIN
LEAF_IN_WEDGE_GE
LEAF_RANK4_CHI_MSB
LEAF_RANK4_CHI_MSB_ALT
LEAF_RANKING_LEMMA
LEAF_RANK_AZIM_INJ
LEAF_RANK_AZIM_NZ
LEAF_RANK_BIJ
LEAF_RANK_COLLINEAR
LEAF_RANK_GG_SUM
LEAF_RANK_GRUTOTI
LEAF_RANK_HAS_SIZE
LEAF_RANK_LEAF
LEAF_RANK_ONTO
LEAF_RANK_PERIODIC
LEAF_RANK_PROPS
LEAF_RANK_REUHADY
LEAF_RANK_SUC_INJ
LEAF_RANK_S_LEAF
LEAF_RANK_TRUNCATE
LEAF_SQRT2
LEAST_BOUND_CC_GG
LEFT_ACTION_LIST_1_EXPLICIT
LEFT_ACTION_LIST_1_PROPERTIES
LEFT_ACTION_LIST_1_PROPERTIES_ALT
LEFT_ACTION_LIST_2_EXISTS
LEFT_ACTION_LIST_3_EXISTS
LEFT_ACTION_LIST_I
LEFT_ACTION_LIST_PROPERTIES
LEFT_AND_EXISTS_THM
LEFT_AND_FORALL_TAG
LEFT_END_POINT
LEFT_IMP_EXISTS_THM
LEFT_IMP_FORALL_TAG
LEFT_INVERSE_EQUATION
LEFT_INVERSE_LINEAR
LEFT_INVERTIBLE_TRANSP
LEFT_MULT_MAP
LEFT_OR_EXISTS_THM
LEFT_OR_FORALL_TAG
LEFT_RIGHT_INVERSES_COINSIDE
LEFT_RIGHT_INVERSE_EQ
LEFT_RIGHT_INVERSE_LINEAR
LEMMA
LEMMA12
LEMMA16_INTERPRETE
LEMMA18
LEMMA20
LEMMA21
LEMMA25
LEMMA26
LEMMA3
LEMMA30
LEMMA33
LEMMA41
LEMMA5
LEMMA52
LEMMA6
LEMMA7
LEMMA81
LEMMA_1834976363
LEMMA_3_POINTS
LEMMA_3_POINTS_FINAL
LEMMA_4828966562
LEMMA_4_POINTS_FINAL
LEMMA_5691615370
LEMMA_6843920790
LEMMA_7175074394
LEMMA_8673686234
LEMMA_CARD_DIFF
LEMMA_FOR_EULER_AFTER_RESCALE
LEMMA_FOR_PAHFWSI
LEMMA_INJ
LEMMA_INJ2
LEMMA_IN_LEMMA42_P25
LEMMA_OF_39
LEMMA_OF_L42
LEMMA_OF_LE20
LEMMA_OF_LEMMA40
LEMMA_PWE1
LEMMA_PWE2
LEMMA_PWE3
LEMMA_PWE4
LEMMA_SUBSET_ORBIT_MAP_LT
LEMMA_SUM_ALL_OVER_CYCLIC_SET
LENGTH1
LENGTH2
LENGTH3
LENGTH4
LENGTH4_SET2
LENGTH4_SET2_SWAP01
LENGTH_1_LEMMA
LENGTH_A_EMPTY
LENGTH_BUTLAST
LENGTH_DROP
LENGTH_EQUA
LENGTH_EQ_EX
LENGTH_IMP_CONS
LENGTH_LEFT_ACTION_LIST
LENGTH_LINEAR_IMAGE
LENGTH_LIST_PAIRS
LENGTH_LIST_PAIRS2
LENGTH_L_SEQ
LENGTH_REVERSE
LENGTH_REVERSE_TABLE
LENGTH_SHIFT_LEFT
LENGTH_SHIFT_RIGHT
LENGTH_TABLE
LENGTH_TRANSLATION
LENGTH_TRUNCATE_SIMPLEX
LENGTH_ZIP
LENGTH_s_init_list
LEOF41
LEPJBDJ
LEPJBDJ_0
LE_0_n
LE_CARDV_IMP_CARD_DETERED
LE_FOR_LEMMA36
LE_MOD_SUC
LE_OF_ZPGPXNN
LE_ORD_IS_ASSYMETRY
LE_PLUS
LE_RIGHT_SUC
LE_SUC_PRE
LE_sqrt8_2
LE_sqrt8_2h0
LFJCIXP
LFLACKU
LFYTDXC
LF_AZIM_CYCLE_EQ_IVS_ND
LIFT_ADD
LIFT_CMUL
LIFT_COMPONENT
LIFT_CONTINUOUS_ATREAL
LIFT_CONTINUOUS_ATREAL_I
LIFT_DIV_CONTINUOUS_ON
LIFT_DOT_CONTINUOUS_ON
LIFT_DROP
LIFT_EQ
LIFT_EQ_CMUL
LIFT_IN_IMAGE_LIFT
LIFT_MUL_CONTINUOUS_ON
LIFT_NEG
LIFT_NORM_CONTINUOUS_ON
LIFT_NUM
LIFT_SUB
LIFT_SUM
LIFT_UPS_CONTINUOUS
LIMPT_APPROACHABLE_FAN
LIMPT_APPROACHABLE_LE_FAN
LIMPT_APPROACHABLE_LIFT_FAN
LIMPT_BALL_FAN
LIMPT_EMPTY_FAN
LIMPT_SEQUENTIAL_FAN
LIMPT_SUBSET_FAN
LIMPT_UNIV_FAN
LIM_ADD_FAN
LIM_AT_FAN
LIM_AT_ID_FAN
LIM_AT_INFINITY_FAN
LIM_AT_WITHIN_FAN
LIM_AT_ZERO_FAN
LIM_CMUL_FAN
LIM_CONST_FAN
LIM_INV_FAN
LIM_IN_SET
LIM_LIFT_DOT_FAN
LIM_LINEAR_FAN
LIM_MATVEC
LIM_NEG_FAN
LIM_NORM_BOUND_FAN
LIM_NULL_CMUL_BOUNDED_FAN
LIM_NULL_FAN
LIM_SEQUENTIALLY_FAN
LIM_SUBSEQUENCE1
LIM_SUBSEQUENCE_FAN
LIM_SUB_FAN
LIM_UNIQUE_FAN
LIM_VECMAT
LIM_WITHIN_FAN
LIM_WITHIN_ID_FAN
LIM_WITHIN_LE_FAN
LIM_WITHIN_OPEN_FAN
LIM_WITHIN_SUBSET_FAN
LINAER_SYM_0
LINDIH_11
LINEAR_0
LINEAR_ADD
LINEAR_BIJECTIVE_LEFT_RIGHT_INVERSE
LINEAR_BOUNDED
LINEAR_BOUNDED_POS
LINEAR_CMUL
LINEAR_COMPONENTWISE
LINEAR_COMPOSE
LINEAR_COMPOSE_ADD
LINEAR_COMPOSE_CMUL
LINEAR_COMPOSE_NEG
LINEAR_COMPOSE_SUB
LINEAR_COMPOSE_VSUM
LINEAR_CONTINUOUS_AT_FAN
LINEAR_CONTINUOUS_COMPOSE
LINEAR_CONTINUOUS_ON_FAN
LINEAR_CONTINUOUS_WITHIN_FAN
LINEAR_EQ
LINEAR_EQ_0
LINEAR_EQ_0_SPAN
LINEAR_EQ_MATRIX
LINEAR_EQ_STDBASIS
LINEAR_FACE
LINEAR_FACE_2
LINEAR_FROM_REALS
LINEAR_FSTCART
LINEAR_I
LINEAR_ID
LINEAR_INDEPENDENT_EXTEND
LINEAR_INDEPENDENT_EXTEND_LEMMA
LINEAR_INDEP_IMAGE_LEMMA
LINEAR_INJECTIVE_0
LINEAR_INJECTIVE_0_SUBSPACE
LINEAR_INJECTIVE_BOUNDED_BELOW_POS
LINEAR_INJECTIVE_IMP_SURJECTIVE
LINEAR_INJECTIVE_ISOMORPHISM
LINEAR_INJECTIVE_LEFT_INVERSE
LINEAR_INVERSE_LEFT
LINEAR_INVERTIBLE_BOUNDED_BELOW
LINEAR_INVERTIBLE_BOUNDED_BELOW_POS
LINEAR_LIFT_COMPONENT
LINEAR_LIFT_DOT
LINEAR_LIM_0_FAN
LINEAR_NEG
LINEAR_NEGATION
LINEAR_PROJECTION
LINEAR_SCALING
LINEAR_SINGULAR_IMAGE_HYPERPLANE
LINEAR_SINGULAR_INTO_HYPERPLANE
LINEAR_SNDCART
LINEAR_SUB
LINEAR_SURJECTIVE_IFF_INJECTIVE
LINEAR_SURJECTIVE_IMP_INJECTIVE
LINEAR_SURJECTIVE_ISOMORPHISM
LINEAR_SURJECTIVE_RIGHT_INVERSE
LINEAR_TO_REALS
LINEAR_VECMAT
LINEAR_VMUL_COMPONENT
LINEAR_VMUL_DROP
LINEAR_VSUM
LINEAR_VSUM_MUL
LINEAR_ZERO
LIN_F_ADD_SINGLE
LIN_F_ADD_SING_LCANCEL
LIN_F_ADD_SING_RCANCEL
LIN_F_APPEND
LIN_F_CONS
LIN_F_EMPTY
LIN_F_EMPTY_LE_0
LIN_F_MUL
LIN_F_MUL_EMPTY
LIN_F_MUL_HD
LIN_F_SUM_EMPTY1
LIN_F_SUM_EMPTY2
LIN_F_SUM_HD
LIN_F_SUM_HD_ZERO
LIN_F_SUM_MOVE1
LIN_F_SUM_MOVE2
LIST_EL_EQ
LIST_EQ_TRUNCATE_SIMPLEX_APPEND_LAST
LIST_EXT_POWER_IN_DARTS
LIST_OF_CC_UH
LIST_OF_DARTS
LIST_OF_DARTS3
LIST_OF_DARTS4
LIST_OF_DARTS_X
LIST_OF_EDGES
LIST_OF_FACES3
LIST_OF_FACES4
LIST_OF_FACES5
LIST_OF_FACES6
LIST_OF_FACES_n
LIST_ORBIT_EXPLICIT
LIST_ORBIT_LEMMA
LIST_PAIRS2
LIST_PAIRS_EMPTY
LIST_PAIRS_NUM_CONS
LIST_PAIRS_NUM_EMPTY
LIST_SUBSET
LIST_SUM
LIST_SUM_A_EMPTY
LIST_SUM_LMUL
LIST_TO
LITTLE_CC_GG3AA
LITTLE_CC_GG3BB
LITTLE_CC_GGA
LITTLE_CC_GGAA
LITTLE_CC_GGB
LITTLE_CC_GGBB
LKGRQUI
LLEEMAA
LLOYXRK1
LLOYXRK2
LM1
LMFUN_INEQ_CENTER_IMP_13
LMFUN_INEQ_CENTER_SUBSET
LMFUN_LE_1
LM_AUX
LOCALIZE_PRESERVE_FACE
LOCAL_CONVEX_NOT_COLLINEAR
LOCAL_CONVEX_NOT_COLLINEAR2
LOCAL_E_SUB_V
LOCAL_FACE_MAP_RHO_NODE1
LOCAL_FAN_AZIM_POS
LOCAL_FAN_CHARACTER_OF_RHO_NODE
LOCAL_FAN_CHARACTER_OF_RHO_NODE2
LOCAL_FAN_CHARACTER_OF_RHO_NODE3
LOCAL_FAN_DUAL_SYM_0
LOCAL_FAN_FACE_FF
LOCAL_FAN_FINITE_FF
LOCAL_FAN_FINITE_V
LOCAL_FAN_IMP_BIJ_FF_NODES
LOCAL_FAN_IMP_CYCLIC_SET
LOCAL_FAN_IMP_FAN
LOCAL_FAN_IMP_FF_SUBSET_DARTS
LOCAL_FAN_IMP_IN_V
LOCAL_FAN_IMP_IN_V2
LOCAL_FAN_IMP_NOT_SEMI_IDE
LOCAL_FAN_IN_FF_DISTINCT
LOCAL_FAN_IN_FF_IN_ORD_PAIRS
LOCAL_FAN_IN_FF_IN_ORD_PAIRS2
LOCAL_FAN_IN_FF_NOT_COLLINEAR
LOCAL_FAN_ITER_IVS_RHO_NODE_IN_V
LOCAL_FAN_ITER_RHO_NODE_IN_V
LOCAL_FAN_IVS_IN_V
LOCAL_FAN_NOT_CARD_FF_GE_2
LOCAL_FAN_NOT_EMPTY_FF
LOCAL_FAN_NOT_SING_FF
LOCAL_FAN_NOT_TWO_V_IN_E
LOCAL_FAN_NOT_V_SING
LOCAL_FAN_ORBIT_MAP_EXPLICIT
LOCAL_FAN_ORBIT_MAP_EXPLICIT_IVS
LOCAL_FAN_ORBIT_MAP_V
LOCAL_FAN_ORBIT_MAP_VITER
LOCAL_FAN_ORBIT_MAP_VITERFF
LOCAL_FAN_RHO_NODE_IVS
LOCAL_FAN_RHO_NODE_PROS
LOCAL_FAN_RHO_NODE_PROS2
LOCAL_FAN_SET_E
LOCAL_FAN_SIMPLE_HYP
LOCAL_FAN_SYM_0
LOCAL_IMP_FINITE_DARTS
LOCAL_RHO_NODE_PAIR_E
LOFA_CARD_EE_V_1
LOFA_CARD_EE_V_2
LOFA_DARTS_FF_UNION_SWITCH_FF
LOFA_DETERMINE_AZIM_IN_FA
LOFA_FST_IDENTIFY
LOFA_HYP_UNION_CARD_GT2
LOFA_IMAGE_RHO_NODE_IDE
LOFA_IMP_AZIM_RHO_NODE_ST
LOFA_IMP_BIJ_VV
LOFA_IMP_CARD_FF_V_EQ
LOFA_IMP_DIS_ELMS
LOFA_IMP_EE_TWO_ELMS
LOFA_IMP_EE_TWO_ELMS_INS_ND
LOFA_IMP_INANGLE_EQ_AZIM
LOFA_IMP_INANGLE_EQ_AZIM_IVS
LOFA_IMP_ITER_IVS_RHO_NODE_ID
LOFA_IMP_ITER_RHO_NODE_ID
LOFA_IMP_LT_CARD_SET_V
LOFA_IMP_LT_CARD_SET_V_ALT
LOFA_IMP_NOT_COLL_IVS
LOFA_IMP_NOT_INCLUDE_VEC0
LOFA_IMP_V_DIFF
LOFA_IN_E_IMP_IN_FF
LOFA_IN_V_SO_DO_RHO_NODE_V
LOFA_V_NOT_EMP
LOFA_V_SUBSET_AFF_HULL
LOOP_MAP_IMP_DIFF_FIRST_ELMS
LOOP_SET_DETER_FIRTS_ELMS
LOOP_SET_ITER_CARD_ID
LOWDIM_EXPAND_BASIS
LOWDIM_EXPAND_DIMENSION
LOWDIM_SUBSET_HYPERPLANE
LT0_LE1
LT1_NZ
LTCTBAN
LT_CARD_MONO_LOFA
LT_PLUS
LT_POW2_COND
LT_PRE
LT_PRE_LE
LT_RIGHT_SUC
LT_SQ8_IMP_LT2
LT_SUC_E
LT_SUC_PRE
LT_n_0
LT_sqrt8_2h0
LUIKGMH
LUNAR_COMM
LUNAR_DEFORM_ARCV_PRESERVED
LUNAR_DEFORM_INJ
LUNAR_DEFORM_ORIGIN
LUNAR_DEFORM_PRESERVE_NORM
LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT
LUNAR_IMP_HALF_CIRCLE_SUBSET_AFF_GT100
LUNAR_IMP_INTERIOR_ANGLE1_EQ_PI
LUNAR_IMP_INTERIOR_ANGLE_EQQ
LUNAR_IMP_IN_TWO_HAFLS_PLANE
LUNAR_IN_V
LVDUCXU
LXDEYBO
L_SEQ_CONS
L_SEQ_NIL
L_SEQ_NN
l_seq
lambda_ext
lambda_oct
lambda_s
lambda_v
lambda_x
lambda_y
last
last1'
law_cosines_126_x
law_cosines_234_x
law_of_cosines
law_of_sines
ldih2_x
ldih2_x_126_s2
ldih2_x_div_sqrtdelta_posbranch
ldih2_x_n
ldih3_x
ldih3_x_135_s2
ldih3_x_div_sqrtdelta_posbranch
ldih3_x_n
ldih5_x_135_s2
ldih5_x_div_sqrtdelta_posbranch
ldih5_x_n
ldih6_x
ldih6_x_126_s2
ldih6_x_div_sqrtdelta_posbranch
ldih6_x_n
ldih_x
ldih_x_126_s2
ldih_x_135_s2
ldih_x_135_s2'
ldih_x_div_sqrtdelta_posbranch
ldih_x_n
le1_82
le1_diag_trape
le_compare_left
le_compare_right
le_hyp_gen
le_list_sum_hyp_gen
leaf
leaf_CIHTIUM
leaf_rank
left_action
left_action_list
left_commutative
left_distributive
left_id
left_injective
left_inverse
left_loop
left_zero
lem
lem1
lem2
lemm_nornal_loop_sub_dart
lemma
lemma'
lemma0
lemma1
lemma2
lemma3
lemma30000
lemma4
lemma5
lemma6
lemma7
lemma8
lemma82_FOCUDTG
lemma8_3_OVOAHCG
lemmaBISHKQW
lemmaCDTETAT
lemmaFKSNTKR
lemmaFOAGLPA
lemmaHOZKXVW
lemmaHQYMRTX
lemmaICJHAOQ
lemmaILTXRQD
lemmaINTERS_HALF_SPACE_DS_FANADD1
lemmaINTERS_HALF_SPACE_DS_FANADD2
lemmaINTERS_HALF_SPACE_DS_FANADD3
lemmaIUCLZYI
lemmaJMKRXLA
lemmaKDAEDEX
lemmaLIPYTUI
lemmaLoopSeparation
lemmaNodalFixedPoint
lemmaParameters
lemmaQF
lemmaQZTPGJV
lemmaQuotientFace
lemmaQuotientNoDoubleJoins
lemmaSGCOSXK
lemmaSTKBEPH
lemmaSZIPOAS
lemmaSimpleQuotient
lemmaTGJISOK
lemmaThreeDarts
lemmaU1_subset_U
lemmaULEKUUB
lemmaZHQCZLX
lemma_1
lemma_2
lemma_3_points
lemma_4_points_circumcenter
lemma_4_points_contradiction
lemma_4_points_rotation1
lemma_4_points_rotation1_full
lemma_4_points_rotation2
lemma_4_points_rotation2_full
lemma_4functions
lemma_5546286427
lemma_CARD_FACE_SET_EQ_3_FULLY_SURROUNDED_FAN
lemma_HYUAZSE
lemma_Moebius_contour_points_subset_darts
lemma_QuotientNode
lemma_add_exponent_function
lemma_add_one_assumption
lemma_add_one_assumption_lt
lemma_atmost_two_orbits
lemma_atom_absorb_quark
lemma_atom_finite
lemma_atom_node_eq
lemma_atom_on_inside_dart
lemma_atom_out_side_loop
lemma_atom_sub_dart_set
lemma_atom_sub_loop
lemma_atom_sub_node
lemma_back_and_next_outside_loop
lemma_back_in_loop
lemma_back_index
lemma_belong
lemma_belong_loop
lemma_border_of_atom
lemma_border_of_atom2
lemma_bound_mInside
lemma_c1
lemma_c11
lemma_c111
lemma_canonical_function
lemma_card_eq
lemma_card_eq_reflect
lemma_card_face_collection
lemma_card_face_walkup_dart
lemma_card_lower_bound
lemma_card_node_eq_set_of_edge
lemma_card_node_eq_set_of_orbits
lemma_card_node_walkup_dart
lemma_card_of_disjoint_covering
lemma_card_partion1_unions_eq
lemma_card_partion2_unions
lemma_card_partion2_unions_approx
lemma_card_partion2_unions_eq
lemma_card_unions_diff
lemma_card_walkup_dart
lemma_category_darts
lemma_ch
lemma_ch1
lemma_ch11
lemma_change_face_walkup
lemma_change_node_walkup
lemma_choice
lemma_choice_function
lemma_choice_in_quotient
lemma_choice_sub_node
lemma_closed_closure
lemma_closed_inters_fan1
lemma_cm3
lemma_complement_path
lemma_complement_two_edges
lemma_component_identity
lemma_component_reflect
lemma_component_representation
lemma_component_subset
lemma_component_symmetry
lemma_component_trans
lemma_congruence_on_face
lemma_congruence_on_loop
lemma_congruence_on_orbit
lemma_connect_hypermap
lemma_contour_in_dart
lemma_convolution_evaluation
lemma_convolution_map
lemma_cycle_eq
lemma_cycle_finite
lemma_cycle_is_face
lemma_cycle_orbit
lemma_cyclic_edge_map
lemma_cyclic_emap
lemma_cyclic_face_map
lemma_cyclic_fmap
lemma_cyclic_hypermap
lemma_cyclic_nmap
lemma_cyclic_node_map
lemma_dart_inside_sub_loop
lemma_dart_invariant
lemma_dart_invariant_power_face
lemma_dart_invariant_power_node
lemma_dart_inveriant_under_inverse_maps
lemma_dart_loop_via_path
lemma_darts_in_contour
lemma_darts_is_Moebius_contour
lemma_darts_on_Moebius_contour
lemma_def_contour
lemma_def_inj_contour
lemma_def_inj_orbit
lemma_def_path
lemma_degenerate_walkup_first_eq
lemma_degenerate_walkup_second_eq
lemma_degenerate_walkup_third_eq
lemma_desc_planar_index
lemma_different_edges
lemma_different_faces
lemma_different_nodes
lemma_disjiont_exists_fan2
lemma_disjiont_exists_fan3
lemma_disjoint_new_loops
lemma_disjoints
lemma_dnax_atomic_structure
lemma_double_shift_non_degenerate
lemma_edge_complement
lemma_edge_cycle
lemma_edge_degenerate
lemma_edge_exception
lemma_edge_from_dart
lemma_edge_identity
lemma_edge_map_walkup_in_dart
lemma_edge_merge
lemma_edge_nondegenerate
lemma_edge_path
lemma_edge_representation
lemma_edge_split
lemma_edge_subset
lemma_edge_subset_component
lemma_edge_walkup
lemma_element_in_list
lemma_eliminate_dart_ouside_Moebius_contour
lemma_eq_iff_shift_eq
lemma_evaluation_complement
lemma_face_contour
lemma_face_contour_on_loop
lemma_face_cycle
lemma_face_degenerate
lemma_face_exception
lemma_face_from_dart
lemma_face_identity
lemma_face_map
lemma_face_map_walkup_in_dart
lemma_face_merge
lemma_face_path
lemma_face_representation
lemma_face_split
lemma_face_subset
lemma_face_subset_component
lemma_face_walkup_eliminate_dart_on_Moebius_contour
lemma_face_walkup_second_segment_contour
lemma_false_loop
lemma_finite_list
lemma_finite_normal_loops
lemma_finite_quotient_darts
lemma_finite_support
lemma_first_dart_on_inj_contour
lemma_fmap
lemma_from_index
lemma_from_index2
lemma_generate_loop
lemma_genex_loop
lemma_geney_loop
lemma_glue_contours
lemma_glue_inj_contours
lemma_glue_inj_lists
lemma_glue_paths
lemma_glueing_condition
lemma_graph
lemma_head
lemma_head_tail
lemma_head_via_restricted
lemma_hypermap1_of_fanx
lemma_hypermap_eq
lemma_hypermap_rep
lemma_identity_atom
lemma_in_QF
lemma_in_QN
lemma_in_QuotientFace
lemma_in_QuotientNode
lemma_in_atom
lemma_in_atom2
lemma_in_canon_darts
lemma_in_components
lemma_in_couple
lemma_in_cycle2
lemma_in_dart
lemma_in_disjoint
lemma_in_dnax
lemma_in_dnax1
lemma_in_dnax2
lemma_in_dnay
lemma_in_dnay1
lemma_in_dnay2
lemma_in_edge
lemma_in_edge2
lemma_in_edge_set
lemma_in_face
lemma_in_face_set
lemma_in_hypermap_orbits
lemma_in_list
lemma_in_list2
lemma_in_loop
lemma_in_node
lemma_in_node1
lemma_in_node2
lemma_in_node3
lemma_in_node_set
lemma_in_orbit
lemma_in_quotient
lemma_in_subset
lemma_in_support
lemma_in_support2
lemma_in_unions
lemma_in_walkup_dart
lemma_inc_injective
lemma_inc_monotone
lemma_inc_not_decreasing
lemma_increasing_index
lemma_increasing_index_one
lemma_indepentdent_complement
lemma_index_on_orbit
lemma_inj_complement
lemma_inj_contour_belong_darts
lemma_inj_contour_via_list
lemma_inj_face_contour
lemma_inj_list
lemma_inj_list2
lemma_inj_loop_path
lemma_inj_node_contour
lemma_inj_orbit
lemma_inj_orbit_via_list
lemma_interior_closure
lemma_inverse_evaluation
lemma_inverse_in_face
lemma_inverse_in_node
lemma_inverse_in_orbit
lemma_inverse_maps_at_nondegenerate_dart
lemma_inverse_on_loop
lemma_inverse_res
lemma_inverses_in_component
lemma_join_contours
lemma_join_inj_contours
lemma_join_inj_lists
lemma_list_disjoint
lemma_list_disjoint1
lemma_list_disjoint2
lemma_list_next
lemma_loop_contour
lemma_loop_eq_face
lemma_loop_identity
lemma_loop_index
lemma_loop_outside_node
lemma_loop_path_via_list
lemma_loop_representation
lemma_lower_bound_index
lemma_mAdd
lemma_mAdd_Exists
lemma_mInside
lemma_mInside_Exists
lemma_mInside_and_length_cycle
lemma_make_contour_loop
lemma_map_next
lemma_marked_dart
lemma_merge_case_count_edges
lemma_minimum_Moebius_hypermap
lemma_new_darts_in_face
lemma_next_exclusive
lemma_next_exclusive2
lemma_next_in_loop
lemma_next_on_normal_loop
lemma_next_power_representation
lemma_nmap
lemma_node_contour
lemma_node_contour_connection
lemma_node_cycle
lemma_node_degenerate
lemma_node_exception
lemma_node_identity
lemma_node_identity_fan
lemma_node_in_support2
lemma_node_inverse_cycle
lemma_node_map
lemma_node_map_walkup_in_dart
lemma_node_merge
lemma_node_nondegenerate
lemma_node_outside_support_darts
lemma_node_path
lemma_node_representation
lemma_node_split
lemma_node_sub_support_darts
lemma_node_subset
lemma_node_subset_component
lemma_node_walkup_eliminate_dart_on_Moebius_contour
lemma_node_walkup_second_segment_contour
lemma_nondegenerate_convolution
lemma_normal_genesis
lemma_not_in_canon_darts
lemma_not_in_list
lemma_not_in_orbit
lemma_not_in_orbit_powers
lemma_null_hypermap_planar_index
lemma_num_partition
lemma_num_partition2
lemma_number_darts_of_inj_contour
lemma_of_lemma82
lemma_on_adding_darts
lemma_on_attach
lemma_on_dnax
lemma_on_dnay
lemma_on_heading
lemma_on_way_going
lemma_one_step_contour
lemma_only_one_component
lemma_only_one_orbit
lemma_orbit_convolution_map
lemma_orbit_disjoint
lemma_orbit_eq
lemma_orbit_finite
lemma_orbit_identity
lemma_orbit_inverse_map_eq
lemma_orbit_of_size_2
lemma_orbit_power
lemma_order_next
lemma_order_permutation
lemma_order_permutation_exists
lemma_pair_eq
lemma_pair_representation
lemma_partition
lemma_partition_by_components
lemma_path_subset
lemma_permutation_via_its_inverse
lemma_permute_loop
lemma_permutes_exception
lemma_permutes_via_surjetive
lemma_planar_hypermap
lemma_planar_index_on_nondegenerate
lemma_planar_index_on_walkup_at_degenerate_dart
lemma_planar_index_on_walkup_at_edge_degenerate_dart
lemma_planar_index_on_walkup_at_isolated_dart
lemma_planar_invariant_shift
lemma_point_in_list
lemma_point_not_in_list
lemma_power_back_and_next_outside_loop
lemma_power_back_in_loop
lemma_power_canon_next
lemma_power_inverse
lemma_power_inverse_in_face
lemma_power_inverse_in_face2
lemma_power_inverse_in_node
lemma_power_inverse_in_node2
lemma_power_inverse_map
lemma_power_next_in_loop
lemma_powers_in_component
lemma_proof0_fan
lemma_proof1_fan
lemma_proof_fan
lemma_properties_of_node_set_fan
lemma_quotient
lemma_r_r'
lemma_r_r'_fix2
lemma_rep_U_fanadd
lemma_representaion_Wf
lemma_representaion_Wn
lemma_reverse_path
lemma_route
lemma_route_exists
lemma_samsara
lemma_samsara_permute
lemma_samsara_power
lemma_second_absorb_quark
lemma_second_inverse_evaluation
lemma_second_inverse_on_loop
lemma_second_on_way_going
lemma_segment_complement
lemma_segment_orbit
lemma_separation_on_loop
lemma_set_disjoint
lemma_shift_component_invariant
lemma_shift_contour
lemma_shift_cycle
lemma_shift_inj_contour
lemma_shift_non_degenerate
lemma_shift_path
lemma_shift_path_evaluation
lemma_simple_hypermap
lemma_singleton_atom
lemma_size
lemma_size_list
lemma_size_of_normal_loop
lemma_split_marked_loop
lemma_splitting_case_count_edges
lemma_sub_inj_contour
lemma_sub_inj_orbit
lemma_sub_list
lemma_sub_part
lemma_sub_support
lemma_sub_two_numbers
lemma_sub_unions_diff
lemma_subcontour
lemma_subpath
lemma_subset
lemma_subset_orbit
lemma_suc_mod
lemma_support_QF
lemma_support_QN
lemma_support_and_atoms
lemma_support_cycle
lemma_support_face_collection
lemma_tail
lemma_tail_via_restricted
lemma_transitive_going
lemma_transitive_permutation
lemma_true_loop
lemma_true_loop1
lemma_true_loop_via_map
lemma_two_series_eq
lemma_unique_head
lemma_unique_tail
lemma_via_inverse_node_map
lemma_walkup_components
lemma_walkup_count_faces
lemma_walkup_count_nodes
lemma_walkup_count_not_splitting_components
lemma_walkup_count_splitting_components
lemma_walkup_edges
lemma_walkup_faces
lemma_walkup_first_component_eq
lemma_walkup_first_edge_eq
lemma_walkup_nodes
lemma_walkup_second_component_eq
lemma_walkup_second_edge_eq
lemma_walkup_support_edges
lemma_yfanadd_aff_ge
lemma_yfanadd_aff_gt
lemma_yfanadd_aff_gt1
lemmaf3
lemmaf32
lemmaf33
lemmaf34
lemmaseoo
leqif
less_polar
let_order_for_loop
lfun
lfun1
lfun_ly
lfun_y1
lhand_subset_rhand
lie_in_half_space_and_azim
lie_in_half_space_and_azim_le
lift
lift6_drop6
lift_6
lim_fan
limit_point_of_fan
lin_approx
lin_combo
lin_f
lindih_gt
lindih_lt
lindihpi_gt
lindihpi_gt_y
lindihpi_lt
lindihpi_lt_y
line
line_exists
line_match_def
line_unique
linear
linear1_aff_fan
linear_aff_fan
linear_inj_fan
linear_inter_normball
list2_INDUCT
list_cases
list_dart_pairs
list_hyp_diag
list_of_darts
list_of_darts3
list_of_darts4
list_of_darts5
list_of_darts6
list_of_dartsX
list_of_edges
list_of_elements
list_of_faces
list_of_faces3
list_of_faces4
list_of_faces456
list_of_faces5
list_of_faces6
list_of_nodes
list_of_vector
list_orbit
list_pairs
list_pairs2
list_prod
list_prod1
list_sum
list_sum2
list_sumn
lite_imp
lite_imp2
lm1
lm2
lm3
lm4
lm5
lm6
lm7
lm9
lm_sub_inc
lmdih0
lmdih2_x_div_sqrtdelta_posbranch
lmdih2_x_n
lmdih3_0
lmdih3_ldih3
lmdih3_x_div_sqrtdelta_posbranch
lmdih3_x_n
lmdih5_0
lmdih5_ldih5
lmdih5_x_div_sqrtdelta_posbranch
lmdih5_x_n
lmdih6_x_div_sqrtdelta_posbranch
lmdih6_x_n
lmdih_ldih
lmdih_x_div_sqrtdelta_posbranch
lmdih_x_n
lmfun
lmfun0
lmfun_bounded
lmfun_h0cut
lmfun_ineq_center
lmfun_inequality
lmfun_lfun
lmfun_lfun2
lmfun_pos_le
lmfun_x
lminus_ge_h0
ln_fan
lnazim
loc_dot
local_fan
local_fan2
localization
logic1
loop_lemma
loop_path
lower_bound_measure_unions_ccube
lp1_th0
lp2_th0
lp3_th0
lp4_th0
lp5_th0
lp_cond
lp_cond_imp_good_list
lp_fan
lp_main_estimate
lp_tau
lunar
lunar_deform
ly
ly_EQ_lmfun