Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2017-07-23 15:16
deb16814
View on Github →
refactor(*): import content from lean/library/data and library_dev
Estimated changes
Created
.gitignore
Created
algebra/group.lean
added
theorem
eq_iff_eq_of_sub_eq_sub
added
theorem
eq_iff_sub_eq_zero
added
theorem
eq_inv_iff_eq_inv
added
theorem
eq_of_mul_inv_eq_one
added
theorem
eq_one_of_inv_eq_one
added
theorem
eq_sub_iff_add_eq
added
theorem
inv_eq_inv_iff_eq
added
theorem
inv_eq_one_iff_eq_one
added
theorem
left_inverse_add_left_sub
added
theorem
left_inverse_add_right_neg_add
added
theorem
left_inverse_inv
added
theorem
left_inverse_neg_add_add_right
added
theorem
left_inverse_sub_add_left
added
theorem
mul_eq_iff_eq_inv_mul
added
theorem
mul_eq_iff_eq_mul_inv
added
theorem
sub_eq_iff_eq_add
Created
algebra/group_power.lean
added
def
gpow
added
theorem
gpow_add
added
theorem
gpow_comm
added
theorem
inv_pow
added
def
monoid.pow
added
theorem
mul_pow
added
theorem
one_pow
added
theorem
pow_add
added
theorem
pow_comm
added
theorem
pow_ge_one_of_ge_one
added
def
pow_int
added
theorem
pow_inv_comm
added
theorem
pow_mul
added
def
pow_nat
added
theorem
pow_one
added
theorem
pow_pos
added
theorem
pow_sub
added
theorem
pow_succ'
added
theorem
pow_succ
added
theorem
pow_zero
Created
algebra/lattice/README.md
Created
algebra/lattice/basic.lean
added
theorem
lattice.bot_inf_eq
added
theorem
lattice.bot_le
added
theorem
lattice.bot_sup_eq
added
theorem
lattice.bot_unique
added
theorem
lattice.eq_bot_iff
added
theorem
lattice.eq_top_iff
added
theorem
lattice.inf_assoc
added
theorem
lattice.inf_bot_eq
added
theorem
lattice.inf_comm
added
theorem
lattice.inf_eq_top_iff
added
theorem
lattice.inf_idem
added
theorem
lattice.inf_le_inf
added
theorem
lattice.inf_le_left
added
theorem
lattice.inf_le_left_of_le
added
theorem
lattice.inf_le_right
added
theorem
lattice.inf_le_right_of_le
added
theorem
lattice.inf_of_le_left
added
theorem
lattice.inf_of_le_right
added
theorem
lattice.inf_sup_self
added
theorem
lattice.inf_top_eq
added
theorem
lattice.le_inf
added
theorem
lattice.le_inf_iff
added
theorem
lattice.le_inf_sup
added
theorem
lattice.le_of_inf_eq
added
theorem
lattice.le_of_sup_eq
added
theorem
lattice.le_sup_left
added
theorem
lattice.le_sup_left_of_le
added
theorem
lattice.le_sup_right
added
theorem
lattice.le_sup_right_of_le
added
theorem
lattice.le_top
added
theorem
lattice.neq_bot_of_le_neq_bot
added
theorem
lattice.sup_assoc
added
theorem
lattice.sup_bot_eq
added
theorem
lattice.sup_comm
added
theorem
lattice.sup_eq_bot_iff
added
theorem
lattice.sup_idem
added
theorem
lattice.sup_inf_le
added
theorem
lattice.sup_inf_self
added
theorem
lattice.sup_le
added
theorem
lattice.sup_le_iff
added
theorem
lattice.sup_le_sup
added
theorem
lattice.sup_of_le_left
added
theorem
lattice.sup_of_le_right
added
theorem
lattice.sup_top_eq
added
theorem
lattice.top_inf_eq
added
theorem
lattice.top_sup_eq
added
theorem
lattice.top_unique
Created
algebra/lattice/basic_experiment.lean
added
theorem
lattice.bot_inf_eq
added
theorem
lattice.bot_le
added
theorem
lattice.bot_sup_eq
added
theorem
lattice.bot_unique
added
theorem
lattice.eq_bot_iff
added
theorem
lattice.eq_top_iff
added
def
lattice.imp
added
theorem
lattice.inf_assoc
added
theorem
lattice.inf_bot_eq
added
theorem
lattice.inf_comm
added
theorem
lattice.inf_eq_top_iff
added
theorem
lattice.inf_idem
added
theorem
lattice.inf_le_inf
added
theorem
lattice.inf_le_left'
added
theorem
lattice.inf_le_left
added
theorem
lattice.inf_le_left_of_le
added
theorem
lattice.inf_le_right'
added
theorem
lattice.inf_le_right
added
theorem
lattice.inf_le_right_of_le
added
theorem
lattice.inf_of_le_left
added
theorem
lattice.inf_of_le_right
added
theorem
lattice.inf_sup_self
added
theorem
lattice.inf_top_eq
added
theorem
lattice.le_bot_iff
added
theorem
lattice.le_inf
added
theorem
lattice.le_inf_iff
added
theorem
lattice.le_inf_sup
added
theorem
lattice.le_of_inf_eq
added
theorem
lattice.le_of_sup_eq
added
theorem
lattice.le_sup_left'
added
theorem
lattice.le_sup_left
added
theorem
lattice.le_sup_left_of_le
added
theorem
lattice.le_sup_right'
added
theorem
lattice.le_sup_right
added
theorem
lattice.le_sup_right_of_le
added
theorem
lattice.le_top
added
theorem
lattice.neq_bot_of_le_neq_bot
added
theorem
lattice.sup_assoc
added
theorem
lattice.sup_bot_eq
added
theorem
lattice.sup_comm
added
theorem
lattice.sup_eq_bot_iff
added
theorem
lattice.sup_idem
added
theorem
lattice.sup_inf_le
added
theorem
lattice.sup_inf_self
added
theorem
lattice.sup_le
added
theorem
lattice.sup_le_iff
added
theorem
lattice.sup_le_sup
added
theorem
lattice.sup_of_le_left
added
theorem
lattice.sup_of_le_right
added
theorem
lattice.sup_top_eq
added
theorem
lattice.top_inf_eq
added
theorem
lattice.top_le_iff
added
theorem
lattice.top_sup_eq
added
theorem
lattice.top_unique
added
theorem
le_antisymm'
Created
algebra/lattice/boolean_algebra.lean
added
theorem
lattice.inf_neg_eq_bot
added
theorem
lattice.inf_sup_left
added
theorem
lattice.inf_sup_right
added
theorem
lattice.le_neg_of_le_neg
added
theorem
lattice.le_sup_inf
added
theorem
lattice.neg_bot
added
theorem
lattice.neg_eq_neg_iff
added
theorem
lattice.neg_eq_neg_of_eq
added
theorem
lattice.neg_inf
added
theorem
lattice.neg_inf_eq_bot
added
theorem
lattice.neg_le_iff_neg_le
added
theorem
lattice.neg_le_neg
added
theorem
lattice.neg_le_neg_iff_le
added
theorem
lattice.neg_le_of_neg_le
added
theorem
lattice.neg_neg
added
theorem
lattice.neg_sup
added
theorem
lattice.neg_sup_eq_top
added
theorem
lattice.neg_top
added
theorem
lattice.neg_unique
added
theorem
lattice.sub_eq
added
theorem
lattice.sub_eq_left
added
theorem
lattice.sup_inf_left
added
theorem
lattice.sup_inf_right
added
theorem
lattice.sup_neg_eq_top
added
theorem
lattice.sup_sub_same
Created
algebra/lattice/bounded_lattice.lean
added
theorem
lattice.monotone_and
added
theorem
lattice.monotone_or
Created
algebra/lattice/bounded_lattice_experiment.lean
added
theorem
lattice.monotone_and
added
theorem
lattice.monotone_or
Created
algebra/lattice/complete_boolean_algebra.lean
added
theorem
lattice.inf_Sup_eq
added
theorem
lattice.neg_Inf
added
theorem
lattice.neg_Sup
added
theorem
lattice.neg_infi
added
theorem
lattice.neg_supr
added
theorem
lattice.sup_Inf_eq
Created
algebra/lattice/complete_lattice.lean
added
def
lattice.Inf
added
theorem
lattice.Inf_empty
added
theorem
lattice.Inf_eq_infi
added
theorem
lattice.Inf_image
added
theorem
lattice.Inf_insert
added
theorem
lattice.Inf_le
added
theorem
lattice.Inf_le_Inf
added
theorem
lattice.Inf_le_Sup
added
theorem
lattice.Inf_le_iff
added
theorem
lattice.Inf_le_of_le
added
theorem
lattice.Inf_singleton
added
theorem
lattice.Inf_union
added
theorem
lattice.Inf_univ
added
def
lattice.Sup
added
theorem
lattice.Sup_empty
added
theorem
lattice.Sup_eq_supr
added
theorem
lattice.Sup_image
added
theorem
lattice.Sup_insert
added
theorem
lattice.Sup_inter_le
added
theorem
lattice.Sup_le
added
theorem
lattice.Sup_le_Sup
added
theorem
lattice.Sup_singleton
added
theorem
lattice.Sup_union
added
theorem
lattice.Sup_univ
added
def
lattice.infi
added
theorem
lattice.infi_and
added
theorem
lattice.infi_comm
added
theorem
lattice.infi_congr_Prop
added
theorem
lattice.infi_const
added
theorem
lattice.infi_empty
added
theorem
lattice.infi_emptyset
added
theorem
lattice.infi_exists
added
theorem
lattice.infi_false
added
theorem
lattice.infi_inf_eq
added
theorem
lattice.infi_infi_eq_left
added
theorem
lattice.infi_infi_eq_right
added
theorem
lattice.infi_insert
added
theorem
lattice.infi_le
added
theorem
lattice.infi_le_infi2
added
theorem
lattice.infi_le_infi
added
theorem
lattice.infi_le_infi_const
added
theorem
lattice.infi_le_of_le
added
theorem
lattice.infi_or
added
theorem
lattice.infi_prod
added
theorem
lattice.infi_sigma
added
theorem
lattice.infi_singleton
added
theorem
lattice.infi_subtype
added
theorem
lattice.infi_sum
added
theorem
lattice.infi_true
added
theorem
lattice.infi_union
added
theorem
lattice.infi_unit
added
theorem
lattice.infi_univ
added
theorem
lattice.insert_of_has_insert
added
theorem
lattice.le_Inf
added
theorem
lattice.le_Inf_inter
added
theorem
lattice.le_Sup
added
theorem
lattice.le_Sup_iff
added
theorem
lattice.le_Sup_of_le
added
theorem
lattice.le_infi
added
theorem
lattice.le_infi_iff
added
theorem
lattice.le_supr
added
theorem
lattice.le_supr_of_le
added
theorem
lattice.monotone_Inf_of_monotone
added
theorem
lattice.monotone_Sup_of_monotone
added
def
lattice.supr
added
theorem
lattice.supr_and
added
theorem
lattice.supr_comm
added
theorem
lattice.supr_congr_Prop
added
theorem
lattice.supr_const
added
theorem
lattice.supr_empty
added
theorem
lattice.supr_emptyset
added
theorem
lattice.supr_exists
added
theorem
lattice.supr_false
added
theorem
lattice.supr_insert
added
theorem
lattice.supr_le
added
theorem
lattice.supr_le_iff
added
theorem
lattice.supr_le_supr2
added
theorem
lattice.supr_le_supr
added
theorem
lattice.supr_le_supr_const
added
theorem
lattice.supr_or
added
theorem
lattice.supr_prod
added
theorem
lattice.supr_sigma
added
theorem
lattice.supr_singleton
added
theorem
lattice.supr_subtype
added
theorem
lattice.supr_sum
added
theorem
lattice.supr_sup_eq
added
theorem
lattice.supr_supr_eq_left
added
theorem
lattice.supr_supr_eq_right
added
theorem
lattice.supr_true
added
theorem
lattice.supr_union
added
theorem
lattice.supr_unit
added
theorem
lattice.supr_univ
added
theorem
set.subset_union_left
added
theorem
set.subset_union_right
Created
algebra/lattice/complete_lattice_experiment.lean
added
theorem
insert_def
added
theorem
insert_eq_of_mem
added
theorem
insert_of_has_insert
added
theorem
inter_def
added
theorem
inter_left_comm
added
def
lattice.Inf
added
theorem
lattice.Inf_empty
added
theorem
lattice.Inf_eq_infi
added
theorem
lattice.Inf_image
added
theorem
lattice.Inf_insert
added
theorem
lattice.Inf_le
added
theorem
lattice.Inf_le_Inf
added
theorem
lattice.Inf_le_Sup
added
theorem
lattice.Inf_le_iff
added
theorem
lattice.Inf_le_of_le
added
theorem
lattice.Inf_singleton
added
theorem
lattice.Inf_union
added
theorem
lattice.Inf_univ
added
def
lattice.Sup
added
theorem
lattice.Sup_empty
added
theorem
lattice.Sup_eq_supr
added
theorem
lattice.Sup_image
added
theorem
lattice.Sup_insert
added
theorem
lattice.Sup_inter_le
added
theorem
lattice.Sup_le
added
theorem
lattice.Sup_le_Sup
added
theorem
lattice.Sup_singleton
added
theorem
lattice.Sup_union
added
theorem
lattice.Sup_univ
added
theorem
lattice.foo'
added
theorem
lattice.foo
added
def
lattice.infi
added
theorem
lattice.infi_and
added
theorem
lattice.infi_comm
added
theorem
lattice.infi_congr_Prop
added
theorem
lattice.infi_const
added
theorem
lattice.infi_empty
added
theorem
lattice.infi_emptyset
added
theorem
lattice.infi_exists
added
theorem
lattice.infi_false
added
theorem
lattice.infi_inf_eq
added
theorem
lattice.infi_infi_eq_left
added
theorem
lattice.infi_infi_eq_right
added
theorem
lattice.infi_insert
added
theorem
lattice.infi_le'
added
theorem
lattice.infi_le
added
theorem
lattice.infi_le_infi2
added
theorem
lattice.infi_le_infi
added
theorem
lattice.infi_le_infi_const
added
theorem
lattice.infi_le_of_le
added
theorem
lattice.infi_or
added
theorem
lattice.infi_prod
added
theorem
lattice.infi_sigma
added
theorem
lattice.infi_singleton
added
theorem
lattice.infi_subtype
added
theorem
lattice.infi_sum
added
theorem
lattice.infi_true
added
theorem
lattice.infi_union
added
theorem
lattice.infi_unit
added
theorem
lattice.infi_univ
added
theorem
lattice.insert_of_has_insert
added
theorem
lattice.le_Inf
added
theorem
lattice.le_Inf_inter
added
theorem
lattice.le_Sup
added
theorem
lattice.le_Sup_iff
added
theorem
lattice.le_Sup_of_le
added
theorem
lattice.le_infi
added
theorem
lattice.le_infi_iff
added
theorem
lattice.le_supr'
added
theorem
lattice.le_supr
added
theorem
lattice.le_supr_of_le
added
theorem
lattice.monotone_Inf_of_monotone
added
theorem
lattice.monotone_Sup_of_monotone
added
def
lattice.supr
added
theorem
lattice.supr_and
added
theorem
lattice.supr_comm
added
theorem
lattice.supr_congr_Prop
added
theorem
lattice.supr_const
added
theorem
lattice.supr_empty
added
theorem
lattice.supr_emptyset
added
theorem
lattice.supr_exists
added
theorem
lattice.supr_false
added
theorem
lattice.supr_insert
added
theorem
lattice.supr_le
added
theorem
lattice.supr_le_iff
added
theorem
lattice.supr_le_supr2
added
theorem
lattice.supr_le_supr
added
theorem
lattice.supr_le_supr_const
added
theorem
lattice.supr_or
added
theorem
lattice.supr_prod
added
theorem
lattice.supr_sigma
added
theorem
lattice.supr_singleton
added
theorem
lattice.supr_subtype
added
theorem
lattice.supr_sum
added
theorem
lattice.supr_sup_eq
added
theorem
lattice.supr_supr_eq_left
added
theorem
lattice.supr_supr_eq_right
added
theorem
lattice.supr_true
added
theorem
lattice.supr_union
added
theorem
lattice.supr_unit
added
theorem
lattice.supr_univ
added
theorem
mem_insert_iff
added
theorem
mem_inter_eq
added
theorem
mem_set_of
added
theorem
mem_set_of_eq
added
theorem
mem_singleton
added
theorem
mem_singleton_iff
added
theorem
mem_union_eq
added
theorem
mem_univ_eq
added
theorem
nmem_set_of_eq
added
theorem
set_eq_def
added
theorem
set_of_false
added
theorem
singleton_def
added
theorem
singleton_eq_singleton_iff
added
theorem
subset_def
added
theorem
subset_insert
added
theorem
subset_univ
added
theorem
union_def
added
theorem
union_left_comm
Created
algebra/lattice/default.lean
Created
algebra/lattice/filter.lean
added
theorem
Union_subset_Union2
added
theorem
Union_subset_Union
added
theorem
Union_subset_Union_const
added
theorem
bind_assoc
added
theorem
compl_image_set_of
added
theorem
diff_empty
added
theorem
diff_neq_empty
added
def
directed
added
theorem
directed_of_chain
added
def
directed_on
added
theorem
directed_on_Union
added
theorem
eq_of_sup_eq_inf_eq
added
theorem
filter.Inf_sets_eq_finite
added
theorem
filter.Inter_mem_sets
added
def
filter.at_bot
added
def
filter.at_top
added
theorem
filter.bind_def
added
theorem
filter.bind_mono2
added
theorem
filter.bind_mono
added
theorem
filter.bind_sup
added
theorem
filter.binfi_sup_eq
added
def
filter.cofinite
added
theorem
filter.empty_in_sets_eq_bot
added
theorem
filter.exists_sets_subset_iff
added
theorem
filter.exists_ultrafilter
added
theorem
filter.filter_eq
added
theorem
filter.filter_eq_bot_of_not_nonempty
added
theorem
filter.fmap_principal
added
theorem
filter.forall_sets_neq_empty_iff_neq_bot
added
theorem
filter.image_mem_map
added
theorem
filter.inf_principal
added
theorem
filter.infi_neq_bot_iff_of_directed
added
theorem
filter.infi_neq_bot_of_directed
added
theorem
filter.infi_sets_eq'
added
theorem
filter.infi_sets_eq
added
theorem
filter.infi_sets_induct
added
theorem
filter.infi_sup_eq
added
theorem
filter.inhabited_of_mem_sets
added
theorem
filter.inter_mem_sets
added
def
filter.join
added
theorem
filter.join_principal_eq_Sup
added
theorem
filter.le_lift'
added
theorem
filter.le_map_vmap
added
theorem
filter.le_of_ultrafilter
added
theorem
filter.le_principal_iff
added
theorem
filter.le_vmap_iff_map_le
added
theorem
filter.le_vmap_map
added
theorem
filter.lift'_cong
added
theorem
filter.lift'_id
added
theorem
filter.lift'_inf_principal_eq
added
theorem
filter.lift'_infi
added
theorem
filter.lift'_lift'_assoc
added
theorem
filter.lift'_lift_assoc
added
theorem
filter.lift'_mono'
added
theorem
filter.lift'_mono
added
theorem
filter.lift'_neq_bot_iff
added
theorem
filter.lift'_principal
added
theorem
filter.lift_assoc
added
theorem
filter.lift_comm
added
theorem
filter.lift_infi'
added
theorem
filter.lift_infi
added
theorem
filter.lift_lift'_assoc
added
theorem
filter.lift_lift'_same_eq_lift'
added
theorem
filter.lift_lift'_same_le_lift'
added
theorem
filter.lift_lift_same_eq_lift
added
theorem
filter.lift_lift_same_le_lift
added
theorem
filter.lift_mono'
added
theorem
filter.lift_mono
added
theorem
filter.lift_neq_bot_iff
added
theorem
filter.lift_principal
added
theorem
filter.lift_sets_eq
added
def
filter.map
added
theorem
filter.map_binfi_eq
added
theorem
filter.map_bot
added
theorem
filter.map_compose
added
theorem
filter.map_eq_bot_iff
added
theorem
filter.map_eq_vmap_of_inverse
added
theorem
filter.map_id
added
theorem
filter.map_infi_eq
added
theorem
filter.map_infi_le
added
theorem
filter.map_lift'_eq2
added
theorem
filter.map_lift'_eq
added
theorem
filter.map_lift_eq2
added
theorem
filter.map_lift_eq
added
theorem
filter.map_mono
added
theorem
filter.map_principal
added
theorem
filter.map_sup
added
theorem
filter.map_swap_vmap_swap_eq
added
theorem
filter.map_vmap_le
added
theorem
filter.mem_bind_sets
added
theorem
filter.mem_bot_sets
added
theorem
filter.mem_inf_sets
added
theorem
filter.mem_inf_sets_of_left
added
theorem
filter.mem_inf_sets_of_right
added
theorem
filter.mem_infi_sets
added
theorem
filter.mem_join_sets
added
theorem
filter.mem_lift'
added
theorem
filter.mem_lift'_iff
added
theorem
filter.mem_lift
added
theorem
filter.mem_lift_iff
added
theorem
filter.mem_map
added
theorem
filter.mem_of_finite_Union_ultrafilter
added
theorem
filter.mem_of_finite_sUnion_ultrafilter
added
theorem
filter.mem_or_compl_mem_of_ultrafilter
added
theorem
filter.mem_or_mem_of_ultrafilter
added
theorem
filter.mem_principal_sets
added
theorem
filter.mem_prod_iff
added
theorem
filter.mem_prod_same_iff
added
theorem
filter.mem_pure
added
theorem
filter.mem_return_sets
added
theorem
filter.mem_sets_of_neq_bot
added
theorem
filter.mem_sup_sets
added
theorem
filter.mem_top_sets_iff
added
theorem
filter.mem_vmap_of_mem
added
theorem
filter.monotone_lift'
added
theorem
filter.monotone_lift
added
theorem
filter.monotone_map
added
theorem
filter.monotone_mem_sets
added
theorem
filter.monotone_principal
added
theorem
filter.monotone_vmap
added
def
filter.principal
added
theorem
filter.principal_bind
added
theorem
filter.principal_empty
added
theorem
filter.principal_eq_bot_iff
added
theorem
filter.principal_eq_iff_eq
added
theorem
filter.principal_le_lift'
added
theorem
filter.principal_mono
added
theorem
filter.principal_univ
added
theorem
filter.prod_comm
added
theorem
filter.prod_inf_prod
added
theorem
filter.prod_lift'_lift'
added
theorem
filter.prod_lift_lift
added
theorem
filter.prod_map_map_eq
added
theorem
filter.prod_mem_prod
added
theorem
filter.prod_mono
added
theorem
filter.prod_neq_bot
added
theorem
filter.prod_principal_principal
added
theorem
filter.prod_same_eq
added
theorem
filter.prod_vmap_vmap_eq
added
theorem
filter.pure_def
added
theorem
filter.return_neq_bot
added
theorem
filter.seq_mono
added
theorem
filter.sup_join
added
theorem
filter.sup_principal
added
theorem
filter.supr_join
added
theorem
filter.supr_map
added
theorem
filter.supr_principal
added
theorem
filter.supr_sets_eq
added
def
filter.towards
added
def
filter.ultrafilter
added
theorem
filter.ultrafilter_map
added
theorem
filter.ultrafilter_of_le
added
theorem
filter.ultrafilter_of_spec
added
theorem
filter.ultrafilter_of_split
added
theorem
filter.ultrafilter_of_ultrafilter
added
theorem
filter.ultrafilter_pure
added
theorem
filter.ultrafilter_ultrafilter_of
added
theorem
filter.ultrafilter_unique
added
theorem
filter.univ_mem_sets'
added
theorem
filter.univ_mem_sets
added
theorem
filter.vimage_mem_vmap
added
def
filter.vmap
added
theorem
filter.vmap_eq_lift'
added
theorem
filter.vmap_lift'_eq2
added
theorem
filter.vmap_lift'_eq
added
theorem
filter.vmap_lift_eq2
added
theorem
filter.vmap_lift_eq
added
theorem
filter.vmap_map
added
theorem
filter.vmap_mono
added
theorem
filter.vmap_neq_bot
added
theorem
filter.vmap_neq_bot_of_surj
added
theorem
filter.vmap_principal
added
theorem
filter.vmap_vmap_comp
added
structure
filter
added
theorem
implies_implies_true_iff
added
theorem
inf_eq_bot_iff_le_compl
added
theorem
lattice.Inf_eq_finite_sets
added
theorem
lattice.Sup_le_iff
added
theorem
map_bind
added
theorem
neg_subset_neg_iff_subset
added
theorem
not_not_mem_iff
added
theorem
prod.fst_swap
added
theorem
prod.mk.eta
added
theorem
prod.snd_swap
added
def
prod.swap
added
theorem
prod.swap_prod_mk
added
theorem
prod.swap_swap
added
theorem
prod.swap_swap_eq
added
theorem
pure_seq_eq_map
added
theorem
sUnion_eq_Union
added
theorem
sUnion_mono
added
theorem
seq_bind_eq
added
theorem
seq_eq_bind_map
added
theorem
set.bind_def
added
theorem
set.diff_right_antimono
added
theorem
set.fmap_eq_image
added
theorem
set.image_eq_vimage_of_inverse
added
theorem
set.image_swap_eq_vimage_swap
added
theorem
set.image_swap_prod
added
theorem
set.mem_image_iff_of_inverse
added
theorem
set.mem_prod_eq
added
theorem
set.mem_seq_iff
added
theorem
set.monotone_inter
added
theorem
set.monotone_prod
added
theorem
set.monotone_set_of
added
theorem
set.ne_empty_iff_exists_mem
added
theorem
set.prod_image_image_eq
added
theorem
set.prod_inter_prod
added
theorem
set.prod_mk_mem_set_prod_eq
added
theorem
set.prod_mono
added
theorem
set.prod_neq_empty_iff
added
theorem
set.prod_singleton_singleton
added
theorem
set.prod_vimage_eq
added
theorem
set.set_of_mem_eq
added
theorem
set.vimage_set_of_eq
added
theorem
singleton_neq_emptyset
added
def
upwards
Created
algebra/lattice/fixed_points.lean
added
theorem
ge_of_eq
added
def
lattice.gfp
added
theorem
lattice.gfp_comp
added
theorem
lattice.gfp_eq
added
theorem
lattice.gfp_gfp
added
theorem
lattice.gfp_induct
added
theorem
lattice.gfp_le
added
theorem
lattice.le_gfp
added
theorem
lattice.le_lfp
added
def
lattice.lfp
added
theorem
lattice.lfp_comp
added
theorem
lattice.lfp_eq
added
theorem
lattice.lfp_induct
added
theorem
lattice.lfp_le
added
theorem
lattice.lfp_lfp
added
theorem
lattice.monotone_gfp
added
theorem
lattice.monotone_lfp
Created
algebra/lattice/zorn.lean
added
def
zorn.chain
added
theorem
zorn.chain_chain_closure
added
inductive
zorn.chain_closure
added
theorem
zorn.chain_closure_closure
added
theorem
zorn.chain_closure_empty
added
theorem
zorn.chain_closure_succ_fixpoint
added
theorem
zorn.chain_closure_succ_fixpoint_iff
added
theorem
zorn.chain_closure_total
added
theorem
zorn.chain_insert
added
theorem
zorn.chain_succ
added
def
zorn.is_max_chain
added
def
zorn.max_chain
added
theorem
zorn.max_chain_spec
added
def
zorn.succ_chain
added
theorem
zorn.succ_increasing
added
theorem
zorn.succ_spec
added
def
zorn.super_chain
added
theorem
zorn.super_of_not_max
added
theorem
zorn.zorn
added
theorem
zorn.zorn_weak_order
Created
algebra/order.lean
added
theorem
comp_le_comp_left_of_monotone
added
theorem
le_dual_eq_le
added
theorem
le_max_left_iff_true
added
theorem
le_max_right_iff_true
added
theorem
max.left_comm
added
theorem
max.right_comm
added
theorem
min_right_comm
added
def
monotone
added
theorem
monotone_app
added
theorem
monotone_comp
added
theorem
monotone_const
added
theorem
monotone_id
added
theorem
monotone_lam
added
def
weak_order_dual
Created
algebra/ring.lean
added
theorem
eq_of_mul_eq_mul_left_of_ne_zero
added
theorem
eq_of_mul_eq_mul_right_of_ne_zero
added
theorem
mul_add_eq_mul_add_iff_sub_mul_add_eq
added
theorem
mul_neg_one_eq_neg
added
theorem
ne_zero_and_ne_zero_of_mul_ne_zero
added
theorem
sub_mul_add_eq_of_mul_add_eq_mul_add
Created
data/bitvec.lean
added
def
bitvec.adc
added
def
bitvec.add_lsb
added
def
bitvec.and
added
def
bitvec.append
added
def
bitvec.bits_to_nat
added
theorem
bitvec.bits_to_nat_to_bool
added
theorem
bitvec.bits_to_nat_to_list
added
def
bitvec.fill_shr
added
def
bitvec.not
added
theorem
bitvec.of_nat_succ
added
def
bitvec.or
added
def
bitvec.sbb
added
def
bitvec.sborrow
added
def
bitvec.sge
added
def
bitvec.sgt
added
def
bitvec.shl
added
def
bitvec.sle
added
def
bitvec.slt
added
def
bitvec.sshr
added
theorem
bitvec.to_nat_append
added
theorem
bitvec.to_nat_of_nat
added
def
bitvec.uborrow
added
def
bitvec.uge
added
def
bitvec.ugt
added
def
bitvec.ule
added
def
bitvec.ult
added
def
bitvec.ushr
added
def
bitvec.xor
added
def
bitvec
Created
data/bool.lean
added
theorem
bool.absurd_of_eq_ff_of_eq_tt
added
theorem
bool.band_assoc
added
theorem
bool.band_comm
added
theorem
bool.band_elim_left
added
theorem
bool.band_elim_right
added
theorem
bool.band_eq_ff
added
theorem
bool.band_eq_tt
added
theorem
bool.band_ff
added
theorem
bool.band_intro
added
theorem
bool.band_left_comm
added
theorem
bool.band_self
added
theorem
bool.band_tt
added
theorem
bool.bnot_bnot
added
theorem
bool.bnot_false
added
theorem
bool.bnot_true
added
theorem
bool.bor_assoc
added
theorem
bool.bor_comm
added
theorem
bool.bor_eq_ff
added
theorem
bool.bor_eq_tt
added
theorem
bool.bor_ff
added
theorem
bool.bor_inl
added
theorem
bool.bor_inr
added
theorem
bool.bor_left_comm
added
theorem
bool.bor_tt
added
def
bool.bxor
added
theorem
bool.bxor_assoc
added
theorem
bool.bxor_comm
added
theorem
bool.bxor_ff
added
theorem
bool.bxor_left_comm
added
theorem
bool.bxor_self
added
theorem
bool.bxor_tt
added
theorem
bool.coe_tt
added
theorem
bool.cond_ff
added
theorem
bool.cond_tt
added
theorem
bool.dichotomy
added
theorem
bool.eq_ff_of_bnot_eq_tt
added
theorem
bool.eq_ff_of_ne_tt
added
theorem
bool.eq_tt_of_bnot_eq_ff
added
theorem
bool.eq_tt_of_ne_ff
added
theorem
bool.ff_band
added
theorem
bool.ff_bor
added
theorem
bool.ff_bxor
added
theorem
bool.ff_bxor_ff
added
theorem
bool.ff_bxor_tt
added
theorem
bool.or_of_bor_eq
added
theorem
bool.tt_band
added
theorem
bool.tt_bor
added
theorem
bool.tt_bxor
added
theorem
bool.tt_bxor_ff
added
theorem
bool.tt_bxor_tt
Created
data/fin.lean
added
theorem
eq_of_lt_succ_of_not_lt
added
theorem
lt_succ_of_lt
added
def
raise_fin
Created
data/hash_map.lean
added
def
bucket_array.as_list
added
def
bucket_array.foldl
added
theorem
bucket_array.foldl_eq
added
theorem
bucket_array.foldl_eq_lem
added
theorem
bucket_array.mem_as_list
added
def
bucket_array.modify
added
def
bucket_array.read
added
def
bucket_array.write
added
def
bucket_array
added
theorem
hash_map.append_of_modify
added
theorem
hash_map.append_of_modify_aux
added
def
hash_map.contains
added
def
hash_map.contains_aux
added
theorem
hash_map.contains_aux_iff
added
theorem
hash_map.contains_iff
added
def
hash_map.entries
added
theorem
hash_map.entries_empty
added
def
hash_map.erase
added
def
hash_map.erase_aux
added
def
hash_map.find
added
def
hash_map.find_aux
added
theorem
hash_map.find_aux_iff
added
theorem
hash_map.find_empty
added
theorem
hash_map.find_erase
added
theorem
hash_map.find_erase_eq
added
theorem
hash_map.find_erase_ne
added
theorem
hash_map.find_iff
added
theorem
hash_map.find_insert
added
theorem
hash_map.find_insert_eq
added
theorem
hash_map.find_insert_ne
added
def
hash_map.fold
added
def
hash_map.insert
added
def
hash_map.insert_all
added
theorem
hash_map.insert_lemma
added
def
hash_map.keys
added
theorem
hash_map.keys_empty
added
theorem
hash_map.mem_erase
added
theorem
hash_map.mem_insert
added
theorem
hash_map.mk_as_list
added
def
hash_map.mk_idx
added
theorem
hash_map.not_contains_empty
added
def
hash_map.of_list
added
def
hash_map.reinsert_aux
added
def
hash_map.replace_aux
added
theorem
hash_map.valid.as_list_length
added
theorem
hash_map.valid.as_list_nodup
added
theorem
hash_map.valid.contains_aux_iff
added
theorem
hash_map.valid.eq'
added
theorem
hash_map.valid.eq
added
theorem
hash_map.valid.erase
added
theorem
hash_map.valid.erase_aux
added
theorem
hash_map.valid.find_aux_iff
added
theorem
hash_map.valid.insert
added
theorem
hash_map.valid.mk
added
theorem
hash_map.valid.modify
added
theorem
hash_map.valid.modify_aux1
added
theorem
hash_map.valid.modify_aux2
added
theorem
hash_map.valid.nodup
added
theorem
hash_map.valid.replace
added
theorem
hash_map.valid.replace_aux
added
def
hash_map.valid
added
theorem
hash_map.valid_aux.eq
added
theorem
hash_map.valid_aux.insert_lemma1
added
theorem
hash_map.valid_aux.nodup
added
theorem
hash_map.valid_aux.unfold_cons
added
inductive
hash_map.valid_aux
added
structure
hash_map
added
def
mk_hash_map
Created
data/int/basic.lean
added
theorem
int.neg_add_neg
added
theorem
int.of_nat_add_neg_succ_of_nat_of_ge
added
theorem
int.of_nat_add_neg_succ_of_nat_of_lt
added
def
nat_succ_eq_int_succ
added
theorem
neg_nat_succ
added
theorem
neg_pred
added
theorem
neg_succ
added
theorem
neg_succ_of_nat_eq'
added
theorem
of_nat_sub
added
def
pred
added
theorem
pred_nat_succ
added
theorem
pred_neg_pred
added
theorem
pred_succ
added
def
rec_nat_on
added
theorem
rec_nat_on_neg
added
def
succ
added
theorem
succ_neg_nat_succ
added
theorem
succ_neg_succ
added
theorem
succ_pred
Created
data/int/order.lean
Created
data/lazy_list.lean
added
def
lazy_list.append
added
def
lazy_list.approx
added
def
lazy_list.filter
added
def
lazy_list.for
added
def
lazy_list.head
added
def
lazy_list.join
added
def
lazy_list.map
added
def
lazy_list.map₂
added
def
lazy_list.nth
added
def
lazy_list.of_list
added
def
lazy_list.singleton
added
def
lazy_list.tail
added
def
lazy_list.to_list
added
def
lazy_list.zip
added
inductive
lazy_list
Created
data/list/basic.lean
added
theorem
list.append.assoc
added
theorem
list.append_concat
added
theorem
list.concat_append
added
theorem
list.concat_cons
added
theorem
list.concat_ne_nil
added
theorem
list.concat_nil
added
theorem
list.cons_inj
added
theorem
list.cons_ne_nil
added
def
list.count
added
theorem
list.count_append
added
theorem
list.count_concat
added
theorem
list.count_cons'
added
theorem
list.count_cons
added
theorem
list.count_cons_ge_count
added
theorem
list.count_cons_of_ne
added
theorem
list.count_cons_self
added
theorem
list.count_eq_zero_of_not_mem
added
theorem
list.count_nil
added
theorem
list.count_pos_of_mem
added
theorem
list.count_singleton
added
theorem
list.head_cons
added
theorem
list.head_eq_of_cons_eq
added
theorem
list.index_of_cons
added
theorem
list.index_of_cons_of_eq
added
theorem
list.index_of_cons_of_ne
added
theorem
list.index_of_le_length
added
theorem
list.index_of_lt_length
added
theorem
list.index_of_nil
added
theorem
list.index_of_nth
added
theorem
list.index_of_of_not_mem
added
def
list.inth
added
theorem
list.inth_succ
added
theorem
list.inth_zero
added
def
list.ith
added
theorem
list.ith_succ
added
theorem
list.ith_zero
added
theorem
list.last_congr
added
theorem
list.last_cons_cons
added
theorem
list.last_singleton
added
theorem
list.length_taken_le
added
theorem
list.mem_iff_count_pos
added
theorem
list.mem_of_count_pos
added
theorem
list.not_mem_of_count_eq_zero
added
theorem
list.not_mem_of_index_of_eq_length
added
theorem
list.nth_eq_some
added
def
list.permutations
added
def
list.permutations_aux.F
added
def
list.permutations_aux.eqn_1
added
def
list.permutations_aux.eqn_2
added
def
list.permutations_aux2
added
def
list.permutations_aux
added
theorem
list.tail_cons
added
theorem
list.tail_eq_of_cons_eq
added
theorem
list.tail_nil
added
theorem
list.taken_all
added
theorem
list.taken_all_of_ge
added
theorem
list.taken_cons
added
theorem
list.taken_nil
added
theorem
list.taken_zero
Created
data/list/comb.lean
added
theorem
list.all_cons
added
theorem
list.all_eq_tt_iff
added
theorem
list.all_eq_tt_of_forall
added
theorem
list.all_nil
added
theorem
list.any_cons
added
theorem
list.any_eq_tt_iff
added
theorem
list.any_nil
added
theorem
list.any_of_mem
added
def
list.decidable_exists_mem
added
def
list.decidable_forall_mem
added
def
list.dinj
added
def
list.dinj₁
added
def
list.dmap
added
theorem
list.dmap_cons_of_neg
added
theorem
list.dmap_cons_of_pos
added
theorem
list.dmap_nil
added
theorem
list.eq_of_mem_map_pair₁
added
theorem
list.exists_mem_cons_iff
added
theorem
list.exists_mem_cons_of
added
theorem
list.exists_mem_cons_of_exists
added
theorem
list.exists_of_any_eq_tt
added
theorem
list.exists_of_mem_dmap
added
def
list.flat
added
theorem
list.foldl_append
added
theorem
list.foldl_cons
added
theorem
list.foldl_eq_foldr
added
theorem
list.foldl_eq_of_comm_of_assoc
added
theorem
list.foldl_nil
added
theorem
list.foldl_reverse
added
theorem
list.foldr_append
added
theorem
list.foldr_cons
added
theorem
list.foldr_nil
added
theorem
list.foldr_reverse
added
theorem
list.forall_mem_cons
added
theorem
list.forall_mem_cons_iff
added
theorem
list.forall_mem_eq_tt_of_all_eq_tt
added
theorem
list.forall_mem_nil
added
theorem
list.forall_mem_of_forall_mem_cons
added
theorem
list.length_mapAccumR
added
theorem
list.length_mapAccumR₂
added
theorem
list.length_map_accumr
added
theorem
list.length_map_accumr₂
added
theorem
list.length_product
added
theorem
list.length_replicate
added
def
list.mapAccumR
added
def
list.mapAccumR₂
added
def
list.map_accumr
added
def
list.map_accumr₂
added
theorem
list.map_dmap_of_inv_of_pos
added
theorem
list.map₂_nil1
added
theorem
list.map₂_nil2
added
theorem
list.mem_dmap
added
theorem
list.mem_of_dinj_of_mem_dmap
added
theorem
list.mem_of_mem_map_pair₁
added
theorem
list.mem_of_mem_product_left
added
theorem
list.mem_of_mem_product_right
added
theorem
list.mem_product
added
theorem
list.nil_product
added
theorem
list.not_exists_mem_nil
added
theorem
list.not_mem_dmap_of_dinj_of_not_mem
added
theorem
list.of_forall_mem_cons
added
theorem
list.or_exists_of_exists_mem_cons
added
def
list.product
added
theorem
list.product_cons
added
theorem
list.product_nil
added
def
list.replicate
added
theorem
list.unzip_cons'
added
theorem
list.unzip_cons
added
theorem
list.unzip_nil
added
theorem
list.zip_cons_cons
added
theorem
list.zip_nil_left
added
theorem
list.zip_nil_right
added
theorem
list.zip_unzip
Created
data/list/default.lean
Created
data/list/perm.lean
added
theorem
list.perm.count_eq_count_of_perm
added
theorem
list.perm.eq_nil_of_perm_nil
added
theorem
list.perm.eq_singleton_of_perm
added
theorem
list.perm.eq_singleton_of_perm_inv
added
theorem
list.perm.eqv
added
theorem
list.perm.erase_perm_erase_of_perm
added
theorem
list.perm.foldl_eq_of_perm
added
theorem
list.perm.foldr_eq_of_perm
added
theorem
list.perm.length_eq_length_of_perm
added
theorem
list.perm.length_eq_of_qeq
added
theorem
list.perm.mem_cons_of_qeq
added
theorem
list.perm.mem_head_of_qeq
added
theorem
list.perm.mem_iff_mem_of_perm
added
theorem
list.perm.mem_of_perm
added
theorem
list.perm.mem_tail_of_qeq
added
theorem
list.perm.nodup_of_perm_of_nodup
added
theorem
list.perm.not_mem_of_perm
added
theorem
list.perm.not_perm_nil_cons
added
theorem
list.perm.perm_app
added
theorem
list.perm.perm_app_comm
added
theorem
list.perm.perm_app_inv
added
theorem
list.perm.perm_app_inv_left
added
theorem
list.perm.perm_app_inv_right
added
theorem
list.perm.perm_app_left
added
theorem
list.perm.perm_app_right
added
theorem
list.perm.perm_cons_app
added
theorem
list.perm.perm_cons_app_cons
added
theorem
list.perm.perm_cons_app_simp
added
theorem
list.perm.perm_cons_inv
added
theorem
list.perm.perm_erase
added
theorem
list.perm.perm_erase_dup_of_perm
added
theorem
list.perm.perm_ext
added
theorem
list.perm.perm_filter
added
theorem
list.perm.perm_iff_forall_count_eq_count
added
theorem
list.perm.perm_iff_forall_mem_count_eq_count
added
theorem
list.perm.perm_induction_on
added
theorem
list.perm.perm_insert
added
theorem
list.perm.perm_insert_insert
added
theorem
list.perm.perm_inter
added
theorem
list.perm.perm_inter_left
added
theorem
list.perm.perm_inter_right
added
theorem
list.perm.perm_inv_core
added
theorem
list.perm.perm_map
added
theorem
list.perm.perm_middle
added
theorem
list.perm.perm_middle_simp
added
theorem
list.perm.perm_of_forall_count_eq
added
theorem
list.perm.perm_of_qeq
added
theorem
list.perm.perm_product
added
theorem
list.perm.perm_product_left
added
theorem
list.perm.perm_product_right
added
theorem
list.perm.perm_rev
added
theorem
list.perm.perm_rev_simp
added
theorem
list.perm.perm_union
added
theorem
list.perm.perm_union_left
added
theorem
list.perm.perm_union_right
added
inductive
list.perm.qeq
added
theorem
list.perm.qeq_app
added
theorem
list.perm.qeq_of_mem
added
theorem
list.perm.qeq_split
added
theorem
list.perm.xswap
added
inductive
list.perm
Created
data/list/set.lean
added
theorem
list.disjoint.comm
added
def
list.disjoint
added
theorem
list.disjoint_append_of_disjoint_left
added
theorem
list.disjoint_cons_of_not_mem_of_disjoint
added
theorem
list.disjoint_left
added
theorem
list.disjoint_nil_left
added
theorem
list.disjoint_nil_right
added
theorem
list.disjoint_of_disjoint_append_left_left
added
theorem
list.disjoint_of_disjoint_append_left_right
added
theorem
list.disjoint_of_disjoint_append_right_left
added
theorem
list.disjoint_of_disjoint_append_right_right
added
theorem
list.disjoint_of_disjoint_cons_left
added
theorem
list.disjoint_of_disjoint_cons_right
added
theorem
list.disjoint_of_nodup_append
added
theorem
list.disjoint_of_subset_left
added
theorem
list.disjoint_of_subset_right
added
theorem
list.disjoint_right
added
theorem
list.dmap_nodup_of_dinj
added
theorem
list.eq_or_mem_of_mem_insert
added
theorem
list.erase_append_left
added
theorem
list.erase_append_right
added
theorem
list.erase_cons
added
theorem
list.erase_cons_head
added
theorem
list.erase_cons_tail
added
def
list.erase_dup
added
theorem
list.erase_dup_cons_of_mem
added
theorem
list.erase_dup_cons_of_not_mem
added
theorem
list.erase_dup_eq_of_nodup
added
theorem
list.erase_dup_nil
added
theorem
list.erase_dup_sublist
added
theorem
list.erase_dup_subset
added
theorem
list.erase_nil
added
theorem
list.erase_of_not_mem
added
theorem
list.erase_sublist
added
theorem
list.erase_subset
added
theorem
list.forall_mem_insert_of_forall_mem
added
theorem
list.forall_mem_inter_of_forall_left
added
theorem
list.forall_mem_inter_of_forall_right
added
theorem
list.forall_mem_of_forall_mem_union_left
added
theorem
list.forall_mem_of_forall_mem_union_right
added
theorem
list.forall_mem_union
added
theorem
list.insert.def
added
theorem
list.insert_nil
added
theorem
list.insert_of_mem
added
theorem
list.insert_of_not_mem
added
theorem
list.inter_cons_of_mem
added
theorem
list.inter_cons_of_not_mem
added
theorem
list.inter_eq_nil_of_disjoint
added
theorem
list.inter_nil
added
theorem
list.length_erase_of_mem
added
theorem
list.length_insert_of_mem
added
theorem
list.length_insert_of_not_mem
added
theorem
list.length_upto
added
theorem
list.lt_of_mem_upto
added
theorem
list.mem_erase_dup
added
theorem
list.mem_erase_dup_iff
added
theorem
list.mem_erase_of_ne_of_mem
added
theorem
list.mem_erase_of_nodup
added
theorem
list.mem_insert_iff
added
theorem
list.mem_insert_of_mem
added
theorem
list.mem_insert_self
added
theorem
list.mem_inter_iff
added
theorem
list.mem_inter_of_mem_of_mem
added
theorem
list.mem_of_mem_erase
added
theorem
list.mem_of_mem_erase_dup
added
theorem
list.mem_of_mem_inter_left
added
theorem
list.mem_of_mem_inter_right
added
theorem
list.mem_or_mem_of_mem_union
added
theorem
list.mem_union_iff
added
theorem
list.mem_union_left
added
theorem
list.mem_union_right
added
theorem
list.mem_upto_of_lt
added
theorem
list.mem_upto_succ_of_mem_upto
added
inductive
list.nodup
added
theorem
list.nodup_app_comm
added
theorem
list.nodup_append_of_nodup_of_nodup_of_disjoint
added
theorem
list.nodup_concat
added
theorem
list.nodup_cons
added
theorem
list.nodup_erase_dup
added
theorem
list.nodup_erase_of_nodup
added
theorem
list.nodup_filter
added
theorem
list.nodup_head
added
theorem
list.nodup_insert
added
theorem
list.nodup_inter_of_nodup
added
theorem
list.nodup_map
added
theorem
list.nodup_middle
added
theorem
list.nodup_nil
added
theorem
list.nodup_of_nodup_append_left
added
theorem
list.nodup_of_nodup_append_right
added
theorem
list.nodup_of_nodup_cons
added
theorem
list.nodup_of_nodup_map
added
theorem
list.nodup_of_sublist
added
theorem
list.nodup_product
added
theorem
list.nodup_singleton
added
theorem
list.nodup_union_of_nodup_of_nodup
added
theorem
list.nodup_upto
added
theorem
list.not_mem_of_nodup_cons
added
theorem
list.not_nodup_cons_of_mem
added
theorem
list.not_nodup_cons_of_not_nodup
added
theorem
list.subset_erase_dup
added
theorem
list.union_cons
added
theorem
list.union_nil
added
def
list.upto
added
theorem
list.upto_ne_nil_of_ne_zero
added
theorem
list.upto_nil
added
theorem
list.upto_step
added
theorem
list.upto_succ
Created
data/list/sort.lean
added
theorem
list.forall_mem_rel_of_sorted_cons
added
def
list.insertion_sort
added
theorem
list.length_split_le
added
theorem
list.length_split_lt
added
def
list.merge
added
def
list.merge_sort
added
theorem
list.merge_sort_cons_cons
added
def
list.ordered_insert
added
theorem
list.perm_insertion_sort
added
theorem
list.perm_merge
added
theorem
list.perm_merge_sort
added
theorem
list.perm_ordered_insert
added
theorem
list.perm_split
added
def
list.sorted
added
theorem
list.sorted_cons
added
theorem
list.sorted_insert_sort
added
theorem
list.sorted_merge
added
theorem
list.sorted_merge_sort
added
theorem
list.sorted_nil
added
theorem
list.sorted_of_sorted_cons
added
theorem
list.sorted_ordered_insert
added
theorem
list.sorted_singleton
added
def
list.split
added
theorem
list.split_cons_of_eq
added
theorem
nat.add_pos_iff_pos_or_pos
added
theorem
nat.add_pos_left
added
theorem
nat.add_pos_right
added
theorem
nat.lt_succ_iff_le
added
theorem
nat.succ_le_succ_iff
Created
data/nat/basic.lean
added
def
iterate
added
theorem
nat.add_eq_addl
added
theorem
nat.add_one
added
theorem
nat.add_one_ne_zero
added
def
nat.addl
added
theorem
nat.addl_succ_left
added
theorem
nat.addl_succ_right
added
theorem
nat.addl_zero_left
added
theorem
nat.addl_zero_right
added
theorem
nat.discriminate
added
theorem
nat.eq_zero_of_add_eq_zero
added
theorem
nat.eq_zero_or_eq_succ_pred
added
theorem
nat.exists_eq_succ_of_ne_zero
added
theorem
nat.one_add
added
theorem
nat.one_succ_zero
added
theorem
nat.sub_induction
added
theorem
nat.succ_add_eq_succ_add
added
theorem
nat.succ_inj
added
theorem
nat.two_step_induction
added
theorem
nat.zero_has_zero
Created
data/nat/bquant.lean
added
def
ball'
added
def
ball
added
theorem
ball_of_ball_succ'
added
theorem
ball_of_ball_succ
added
theorem
ball_succ_of_ball
added
theorem
ball_zero'
added
theorem
ball_zero
added
theorem
not_ball_of_not
added
theorem
not_ball_succ_of_not_ball
added
def
step_p
Created
data/nat/gcd.lean
added
theorem
nat.comprime_one_left
added
theorem
nat.comprime_one_right
added
theorem
nat.coprime_div_gcd_div_gcd
added
theorem
nat.coprime_mul
added
theorem
nat.coprime_mul_right
added
theorem
nat.coprime_of_coprime_dvd_left
added
theorem
nat.coprime_of_coprime_dvd_right
added
theorem
nat.coprime_of_coprime_mul_left
added
theorem
nat.coprime_of_coprime_mul_left_right
added
theorem
nat.coprime_of_coprime_mul_right
added
theorem
nat.coprime_of_coprime_mul_right_right
added
theorem
nat.coprime_of_dvd'
added
theorem
nat.coprime_of_dvd
added
theorem
nat.coprime_pow
added
theorem
nat.coprime_pow_left
added
theorem
nat.coprime_pow_right
added
theorem
nat.coprime_swap
added
theorem
nat.dvd_gcd
added
theorem
nat.dvd_lcm_left
added
theorem
nat.dvd_lcm_right
added
theorem
nat.dvd_of_coprime_of_dvd_mul_left
added
theorem
nat.dvd_of_coprime_of_dvd_mul_right
added
theorem
nat.eq_zero_of_gcd_eq_zero_left
added
theorem
nat.eq_zero_of_gcd_eq_zero_right
added
theorem
nat.exists_coprime
added
theorem
nat.exists_eq_prod_and_dvd_and_dvd
added
theorem
nat.gcd_assoc
added
theorem
nat.gcd_comm
added
theorem
nat.gcd_div
added
theorem
nat.gcd_dvd
added
theorem
nat.gcd_dvd_gcd_mul_left
added
theorem
nat.gcd_dvd_gcd_mul_left_right
added
theorem
nat.gcd_dvd_gcd_mul_right
added
theorem
nat.gcd_dvd_gcd_mul_right_right
added
theorem
nat.gcd_dvd_gcd_of_dvd_left
added
theorem
nat.gcd_dvd_gcd_of_dvd_right
added
theorem
nat.gcd_dvd_left
added
theorem
nat.gcd_dvd_right
added
theorem
nat.gcd_eq_one_of_coprime
added
theorem
nat.gcd_mul_lcm
added
theorem
nat.gcd_mul_left
added
theorem
nat.gcd_mul_left_cancel_of_coprime
added
theorem
nat.gcd_mul_left_cancel_of_coprime_right
added
theorem
nat.gcd_mul_right
added
theorem
nat.gcd_mul_right_cancel_of_coprime
added
theorem
nat.gcd_mul_right_cancel_of_coprime_right
added
theorem
nat.gcd_one_right
added
theorem
nat.gcd_pos_of_pos_left
added
theorem
nat.gcd_pos_of_pos_right
added
theorem
nat.lcm_assoc
added
theorem
nat.lcm_comm
added
theorem
nat.lcm_dvd
added
theorem
nat.lcm_one_left
added
theorem
nat.lcm_one_right
added
theorem
nat.lcm_self
added
theorem
nat.lcm_zero_left
added
theorem
nat.lcm_zero_right
added
theorem
nat.not_coprime_of_dvd_of_dvd
Created
data/nat/sub.lean
added
theorem
nat.dist.def
added
theorem
nat.dist.triangle_inequality
added
def
nat.dist
added
theorem
nat.dist_add_add_left
added
theorem
nat.dist_add_add_right
added
theorem
nat.dist_comm
added
theorem
nat.dist_eq_intro
added
theorem
nat.dist_eq_sub_of_ge
added
theorem
nat.dist_eq_sub_of_le
added
theorem
nat.dist_eq_zero
added
theorem
nat.dist_mul_left
added
theorem
nat.dist_mul_right
added
theorem
nat.dist_pos_of_ne
added
theorem
nat.dist_self
added
theorem
nat.dist_succ_succ
added
theorem
nat.dist_zero_left
added
theorem
nat.dist_zero_right
added
theorem
nat.eq_of_dist_eq_zero
Created
data/num/basic.lean
added
def
cast_num
added
def
cast_pos_num
added
def
int.of_snum
added
def
int.of_znum
added
def
nat.of_num
added
def
nat.of_pos_num
added
def
num.bit
added
def
num.cmp
added
def
num.of_nat
added
def
num.pred
added
def
num.size
added
def
num.succ'
added
def
num.succ
added
def
num.to_znum
added
inductive
num
added
def
nzsnum.bit0
added
def
nzsnum.bit1
added
def
nzsnum.drec'
added
def
nzsnum.head
added
def
nzsnum.not
added
def
nzsnum.sign
added
def
nzsnum.tail
added
inductive
nzsnum
added
def
pos_num.bit
added
def
pos_num.cmp
added
def
pos_num.is_one
added
def
pos_num.of_nat
added
def
pos_num.of_nat_succ
added
def
pos_num.pred'
added
def
pos_num.pred
added
def
pos_num.psub
added
def
pos_num.size
added
def
pos_num.succ
added
inductive
pos_num
added
def
snum.bit0
added
def
snum.bit1
added
def
snum.bit
added
theorem
snum.bit_one
added
theorem
snum.bit_zero
added
def
snum.bits
added
def
snum.cadd
added
def
snum.czadd
added
def
snum.drec'
added
def
snum.head
added
def
snum.not
added
def
snum.pred
added
def
snum.rec'
added
def
snum.sign
added
def
snum.succ
added
def
snum.tail
added
def
snum.test_bit
added
inductive
snum
added
def
znum.pred
added
def
znum.succ
added
def
znum.zneg
added
inductive
znum
Created
data/num/bitwise.lean
added
def
num.land
added
def
num.ldiff
added
def
num.lor
added
def
num.lxor
added
def
num.one_bits
added
def
num.shiftl
added
def
num.shiftr
added
def
num.test_bit
added
def
pos_num.land
added
def
pos_num.ldiff
added
def
pos_num.lor
added
def
pos_num.lxor
added
def
pos_num.one_bits
added
def
pos_num.shiftl
added
def
pos_num.shiftr
added
def
pos_num.test_bit
Created
data/num/lemmas.lean
added
theorem
num.add_of_nat
added
theorem
num.add_succ
added
theorem
num.add_to_nat
added
theorem
num.add_zero
added
theorem
num.bit_to_nat
added
theorem
num.bitwise_to_nat
added
theorem
num.cmp_dec
added
theorem
num.cmp_swap
added
theorem
num.land_to_nat
added
theorem
num.ldiff_to_nat
added
theorem
num.le_iff_cmp
added
theorem
num.lor_to_nat
added
theorem
num.lt_iff_cmp
added
theorem
num.lxor_to_nat
added
theorem
num.mul_to_nat
added
theorem
num.of_nat_inj
added
theorem
num.of_to_nat
added
theorem
num.one_to_nat
added
theorem
num.pred_to_nat
added
theorem
num.shiftl_to_nat
added
theorem
num.shiftr_to_nat
added
theorem
num.succ'_to_nat
added
theorem
num.succ_to_nat
added
theorem
num.test_bit_to_nat
added
theorem
num.to_nat_inj
added
theorem
num.to_of_nat
added
theorem
num.zero_add
added
theorem
num.zero_to_nat
added
theorem
pos_num.add_one
added
theorem
pos_num.add_succ
added
theorem
pos_num.add_to_nat
added
theorem
pos_num.bit0_of_bit0
added
theorem
pos_num.bit1_of_bit1
added
theorem
pos_num.bit_to_nat
added
theorem
pos_num.cmp_dec
added
theorem
pos_num.cmp_dec_lemma
added
theorem
pos_num.cmp_swap
added
theorem
pos_num.le_iff_cmp
added
theorem
pos_num.lt_iff_cmp
added
theorem
pos_num.mul_to_nat
added
theorem
pos_num.of_to_nat
added
theorem
pos_num.one_add
added
theorem
pos_num.one_to_nat
added
theorem
pos_num.pred'_to_nat
added
theorem
pos_num.pred_to_nat
added
theorem
pos_num.succ_to_nat
added
theorem
pos_num.to_nat_inj
added
theorem
pos_num.to_nat_pos
Created
data/pfun.lean
added
def
pfun.as_subtype
added
theorem
pfun.bind_defined
added
def
pfun.dom
added
theorem
pfun.dom_iff_graph
added
def
pfun.eval_opt
added
def
pfun.fn
added
def
pfun.graph
added
theorem
pfun.pure_defined
added
def
pfun.ran
added
def
pfun.restrict
added
def
pfun
added
def
roption.assert
added
theorem
roption.assert_defined
added
theorem
roption.bind_assoc
added
theorem
roption.bind_defined
added
theorem
roption.bind_some_eq_map
added
theorem
roption.dom_iff_mem
added
theorem
roption.eq_ret_of_mem
added
theorem
roption.exists_of_mem_bind
added
theorem
roption.mem_bind
added
theorem
roption.mem_ret
added
theorem
roption.mem_ret_iff
added
theorem
roption.mem_some
added
theorem
roption.mem_unique
added
def
roption.of_option
added
theorem
roption.of_to_option
added
def
roption.restrict
added
theorem
roption.some_bind
added
theorem
roption.to_of_option
added
def
roption.to_option
added
structure
roption
Created
data/pnat.lean
added
def
nat.succ_pnat
added
def
nat.to_pnat'
added
def
nat.to_pnat
added
theorem
pnat.nat_coe_val
added
theorem
pnat.to_pnat'_coe
added
theorem
pnat.to_pnat'_val
added
def
pnat
Created
data/rat.lean
added
def
linear_order_cases_on
added
theorem
linear_order_cases_on_eq
added
theorem
linear_order_cases_on_gt
added
theorem
linear_order_cases_on_lt
added
theorem
mul_nonneg_iff_right_nonneg_of_pos
added
theorem
not_antimono
added
def
rat.decidable_nonneg
added
def
rat
Created
data/seq/computation.lean
added
def
computation.bind.F
added
def
computation.bind.G
added
def
computation.bind
added
theorem
computation.bind_assoc
added
theorem
computation.bind_congr
added
theorem
computation.bind_promises
added
theorem
computation.bind_ret'
added
theorem
computation.bind_ret
added
def
computation.bisim_o
added
def
computation.cases_on
added
def
computation.corec.F
added
def
computation.corec
added
def
computation.corec_eq
added
def
computation.destruct
added
theorem
computation.destruct_empty
added
theorem
computation.destruct_eq_ret
added
theorem
computation.destruct_eq_think
added
theorem
computation.destruct_map
added
theorem
computation.destruct_ret
added
theorem
computation.destruct_think
added
def
computation.empty
added
theorem
computation.empty_orelse
added
theorem
computation.empty_promises
added
theorem
computation.eq_empty_of_not_terminates
added
theorem
computation.eq_of_bisim
added
theorem
computation.eq_of_ret_mem
added
def
computation.eq_thinkN'
added
def
computation.eq_thinkN
added
theorem
computation.equiv.equivalence
added
theorem
computation.equiv.refl
added
theorem
computation.equiv.symm
added
theorem
computation.equiv.trans
added
def
computation.equiv
added
theorem
computation.equiv_of_mem
added
theorem
computation.equiv_ret_of_mem
added
theorem
computation.exists_of_lift_rel_left
added
theorem
computation.exists_of_lift_rel_right
added
theorem
computation.exists_of_mem_bind
added
theorem
computation.exists_of_mem_map
added
def
computation.exists_results_of_mem
added
def
computation.get
added
theorem
computation.get_bind
added
def
computation.get_eq_of_mem
added
def
computation.get_eq_of_promises
added
theorem
computation.get_equiv
added
def
computation.get_mem
added
def
computation.get_promises
added
theorem
computation.get_ret
added
theorem
computation.get_think
added
theorem
computation.get_thinkN
added
theorem
computation.has_bind_eq_bind
added
theorem
computation.has_map_eq_map
added
def
computation.head
added
theorem
computation.head_empty
added
theorem
computation.head_ret
added
theorem
computation.head_think
added
def
computation.is_bisimulation
added
def
computation.join
added
theorem
computation.le_stable
added
def
computation.length
added
theorem
computation.length_bind
added
theorem
computation.length_ret
added
theorem
computation.length_think
added
theorem
computation.length_thinkN
added
theorem
computation.lift_eq_iff_equiv
added
def
computation.lift_rel.equiv
added
def
computation.lift_rel.imp
added
def
computation.lift_rel.refl
added
theorem
computation.lift_rel.swap
added
def
computation.lift_rel.symm
added
def
computation.lift_rel.trans
added
def
computation.lift_rel
added
def
computation.lift_rel_aux.ret_left
added
def
computation.lift_rel_aux.ret_right
added
theorem
computation.lift_rel_aux.swap
added
def
computation.lift_rel_aux
added
theorem
computation.lift_rel_bind
added
theorem
computation.lift_rel_congr
added
theorem
computation.lift_rel_def
added
theorem
computation.lift_rel_map
added
theorem
computation.lift_rel_mem_cases
added
theorem
computation.lift_rel_of_mem
added
theorem
computation.lift_rel_rec.lem
added
theorem
computation.lift_rel_rec
added
theorem
computation.lift_rel_return
added
theorem
computation.lift_rel_return_left
added
theorem
computation.lift_rel_return_right
added
theorem
computation.lift_rel_think_left
added
theorem
computation.lift_rel_think_right
added
def
computation.lmap
added
def
computation.map
added
theorem
computation.map_comp
added
theorem
computation.map_congr
added
theorem
computation.map_id
added
theorem
computation.map_ret'
added
theorem
computation.map_ret
added
theorem
computation.map_think'
added
theorem
computation.map_think
added
theorem
computation.mem_bind
added
theorem
computation.mem_map
added
def
computation.mem_of_get_eq
added
def
computation.mem_of_promises
added
theorem
computation.mem_promises
added
def
computation.mem_rec_on
added
theorem
computation.mem_unique
added
theorem
computation.not_mem_empty
added
theorem
computation.not_terminates_empty
added
theorem
computation.of_results_bind
added
theorem
computation.of_results_think
added
theorem
computation.of_thinkN_terminates
added
theorem
computation.of_think_mem
added
theorem
computation.of_think_terminates
added
def
computation.orelse
added
theorem
computation.orelse_empty
added
theorem
computation.orelse_ret
added
theorem
computation.orelse_think
added
def
computation.promises
added
theorem
computation.promises_congr
added
def
computation.rel_of_lift_rel
added
def
computation.results.len_unique
added
def
computation.results.length
added
def
computation.results.mem
added
def
computation.results.terminates
added
def
computation.results.val_unique
added
def
computation.results
added
theorem
computation.results_bind
added
def
computation.results_of_terminates'
added
def
computation.results_of_terminates
added
theorem
computation.results_ret
added
theorem
computation.results_think
added
theorem
computation.results_thinkN
added
theorem
computation.results_thinkN_ret
added
theorem
computation.results_think_iff
added
theorem
computation.ret_bind
added
theorem
computation.ret_mem
added
theorem
computation.ret_orelse
added
def
computation.return
added
theorem
computation.return_def
added
def
computation.rmap
added
def
computation.run_for
added
def
computation.tail
added
theorem
computation.tail_empty
added
theorem
computation.tail_ret
added
theorem
computation.tail_think
added
def
computation.terminates
added
theorem
computation.terminates_congr
added
theorem
computation.terminates_def
added
theorem
computation.terminates_map_iff
added
def
computation.terminates_of_lift_rel
added
theorem
computation.terminates_of_mem
added
def
computation.terminates_rec_on
added
def
computation.think
added
def
computation.thinkN
added
theorem
computation.thinkN_equiv
added
theorem
computation.thinkN_mem
added
theorem
computation.think_bind
added
theorem
computation.think_empty
added
theorem
computation.think_equiv
added
theorem
computation.think_mem
added
def
computation
Created
data/seq/parallel.lean
added
theorem
computation.exists_of_mem_parallel
added
theorem
computation.map_parallel
added
theorem
computation.mem_parallel
added
def
computation.parallel.aux1
added
def
computation.parallel.aux2
added
def
computation.parallel
added
theorem
computation.parallel_congr_left
added
theorem
computation.parallel_congr_lem
added
theorem
computation.parallel_congr_right
added
theorem
computation.parallel_empty
added
theorem
computation.parallel_promises
added
def
computation.parallel_rec
added
theorem
computation.terminates_parallel.aux
added
theorem
computation.terminates_parallel
Created
data/seq/seq.lean
added
def
seq.append
added
theorem
seq.append_assoc
added
theorem
seq.append_nil
added
def
seq.bisim_o
added
def
seq.cases_on
added
theorem
seq.coinduction2
added
theorem
seq.coinduction
added
def
seq.cons
added
theorem
seq.cons_append
added
def
seq.corec.F
added
def
seq.corec
added
def
seq.corec_eq
added
def
seq.destruct
added
theorem
seq.destruct_cons
added
theorem
seq.destruct_eq_cons
added
theorem
seq.destruct_eq_nil
added
theorem
seq.destruct_nil
added
def
seq.drop
added
theorem
seq.dropn_add
added
theorem
seq.dropn_tail
added
theorem
seq.eq_of_bisim
added
theorem
seq.eq_or_mem_of_mem_cons
added
theorem
seq.exists_of_mem_map
added
def
seq.head
added
theorem
seq.head_cons
added
theorem
seq.head_dropn
added
theorem
seq.head_eq_destruct
added
theorem
seq.head_nil
added
def
seq.is_bisimulation
added
def
seq.join
added
theorem
seq.join_append
added
theorem
seq.join_cons
added
theorem
seq.join_cons_cons
added
theorem
seq.join_cons_nil
added
theorem
seq.join_nil
added
theorem
seq.le_stable
added
def
seq.map
added
theorem
seq.map_append
added
theorem
seq.map_comp
added
theorem
seq.map_cons
added
theorem
seq.map_id
added
theorem
seq.map_nil
added
theorem
seq.map_nth
added
theorem
seq.map_tail
added
def
seq.mem_append_left
added
theorem
seq.mem_cons
added
theorem
seq.mem_cons_iff
added
theorem
seq.mem_cons_of_mem
added
theorem
seq.mem_map
added
theorem
seq.mem_rec_on
added
def
seq.nil
added
theorem
seq.nil_append
added
theorem
seq.not_mem_nil
added
def
seq.nth
added
theorem
seq.nth_tail
added
def
seq.of_lazy_list
added
def
seq.of_list
added
def
seq.of_list_append
added
def
seq.of_list_cons
added
def
seq.of_list_nil
added
def
seq.of_mem_append
added
def
seq.of_stream
added
def
seq.of_stream_append
added
def
seq.of_stream_cons
added
def
seq.omap
added
def
seq.split_at
added
def
seq.tail
added
theorem
seq.tail_cons
added
theorem
seq.tail_nil
added
def
seq.take
added
def
seq.to_list'
added
def
seq.to_list
added
def
seq.to_list_or_stream
added
def
seq.to_stream
added
def
seq.unzip
added
def
seq.zip
added
def
seq.zip_with
added
def
seq1.bind
added
theorem
seq1.bind_assoc
added
theorem
seq1.bind_ret
added
def
seq1.join
added
theorem
seq1.join_cons
added
theorem
seq1.join_join
added
theorem
seq1.join_map_ret
added
theorem
seq1.join_nil
added
def
seq1.map
added
theorem
seq1.map_id
added
theorem
seq1.map_join'
added
theorem
seq1.map_join
added
def
seq1.ret
added
theorem
seq1.ret_bind
added
def
seq1.to_seq
added
def
seq1
added
def
seq
Created
data/seq/wseq.lean
added
def
wseq.all
added
def
wseq.any
added
def
wseq.append
added
theorem
wseq.append_assoc
added
theorem
wseq.append_nil
added
def
wseq.bind
added
theorem
wseq.bind_assoc
added
theorem
wseq.bind_congr
added
theorem
wseq.bind_ret
added
theorem
wseq.bisim_o.imp
added
def
wseq.bisim_o
added
def
wseq.cases_on
added
def
wseq.collect
added
def
wseq.compute
added
def
wseq.cons
added
theorem
wseq.cons_append
added
theorem
wseq.cons_congr
added
def
wseq.destruct
added
def
wseq.destruct_append.aux
added
theorem
wseq.destruct_append
added
theorem
wseq.destruct_congr
added
theorem
wseq.destruct_congr_iff
added
theorem
wseq.destruct_cons
added
theorem
wseq.destruct_dropn
added
theorem
wseq.destruct_flatten
added
def
wseq.destruct_join.aux
added
theorem
wseq.destruct_join
added
theorem
wseq.destruct_map
added
theorem
wseq.destruct_nil
added
theorem
wseq.destruct_of_seq
added
theorem
wseq.destruct_some_of_destruct_tail_some
added
theorem
wseq.destruct_tail
added
theorem
wseq.destruct_terminates_of_nth_terminates
added
theorem
wseq.destruct_think
added
def
wseq.drop.aux
added
def
wseq.drop.aux_none
added
def
wseq.drop
added
theorem
wseq.dropn_add
added
theorem
wseq.dropn_congr
added
theorem
wseq.dropn_cons
added
theorem
wseq.dropn_nil
added
theorem
wseq.dropn_of_seq
added
theorem
wseq.dropn_tail
added
theorem
wseq.dropn_think
added
theorem
wseq.eq_or_mem_iff_mem
added
theorem
wseq.equiv.equivalence
added
theorem
wseq.equiv.ext
added
theorem
wseq.equiv.refl
added
theorem
wseq.equiv.symm
added
theorem
wseq.equiv.trans
added
def
wseq.equiv
added
theorem
wseq.exists_dropn_of_mem
added
theorem
wseq.exists_nth_of_mem
added
theorem
wseq.exists_of_lift_rel_left
added
theorem
wseq.exists_of_lift_rel_right
added
theorem
wseq.exists_of_mem_bind
added
theorem
wseq.exists_of_mem_join
added
theorem
wseq.exists_of_mem_map
added
def
wseq.filter
added
def
wseq.filter_map
added
def
wseq.find
added
def
wseq.find_index
added
def
wseq.find_indexes
added
def
wseq.flatten
added
theorem
wseq.flatten_congr
added
theorem
wseq.flatten_equiv
added
theorem
wseq.flatten_ret
added
theorem
wseq.flatten_think
added
def
wseq.get
added
def
wseq.head
added
theorem
wseq.head_congr
added
theorem
wseq.head_cons
added
theorem
wseq.head_nil
added
theorem
wseq.head_of_seq
added
theorem
wseq.head_some_of_head_tail_some
added
theorem
wseq.head_some_of_nth_some
added
theorem
wseq.head_terminates_iff
added
theorem
wseq.head_terminates_of_head_tail_terminates
added
theorem
wseq.head_terminates_of_mem
added
theorem
wseq.head_terminates_of_nth_terminates
added
theorem
wseq.head_think
added
def
wseq.index_of
added
def
wseq.indexes_of
added
def
wseq.inits
added
def
wseq.is_empty
added
def
wseq.is_finite
added
def
wseq.join
added
theorem
wseq.join_append
added
theorem
wseq.join_congr
added
def
wseq.join_cons
added
theorem
wseq.join_join
added
theorem
wseq.join_map_ret
added
def
wseq.join_nil
added
theorem
wseq.join_ret
added
def
wseq.join_think
added
def
wseq.length
added
theorem
wseq.length_eq_map
added
def
wseq.lift_rel.equiv
added
def
wseq.lift_rel.refl
added
def
wseq.lift_rel.swap
added
def
wseq.lift_rel.swap_lem
added
def
wseq.lift_rel.symm
added
def
wseq.lift_rel.trans
added
def
wseq.lift_rel
added
theorem
wseq.lift_rel_append
added
theorem
wseq.lift_rel_bind
added
def
wseq.lift_rel_cons
added
theorem
wseq.lift_rel_destruct
added
theorem
wseq.lift_rel_destruct_iff
added
theorem
wseq.lift_rel_dropn_destruct
added
theorem
wseq.lift_rel_flatten
added
theorem
wseq.lift_rel_join.lem
added
theorem
wseq.lift_rel_join
added
theorem
wseq.lift_rel_map
added
def
wseq.lift_rel_nil
added
theorem
wseq.lift_rel_o.imp
added
theorem
wseq.lift_rel_o.imp_right
added
def
wseq.lift_rel_o.swap
added
def
wseq.lift_rel_o
added
def
wseq.lift_rel_think_left
added
def
wseq.lift_rel_think_right
added
def
wseq.map
added
theorem
wseq.map_append
added
theorem
wseq.map_comp
added
theorem
wseq.map_congr
added
theorem
wseq.map_cons
added
theorem
wseq.map_id
added
theorem
wseq.map_join
added
theorem
wseq.map_nil
added
theorem
wseq.map_ret
added
theorem
wseq.map_think
added
def
wseq.mem_append_left
added
theorem
wseq.mem_congr
added
theorem
wseq.mem_cons
added
theorem
wseq.mem_cons_iff
added
theorem
wseq.mem_cons_of_mem
added
theorem
wseq.mem_map
added
theorem
wseq.mem_of_mem_dropn
added
theorem
wseq.mem_of_mem_tail
added
theorem
wseq.mem_rec_on
added
theorem
wseq.mem_think
added
def
wseq.nil
added
theorem
wseq.nil_append
added
theorem
wseq.not_mem_nil
added
def
wseq.nth
added
theorem
wseq.nth_add
added
theorem
wseq.nth_congr
added
theorem
wseq.nth_mem
added
theorem
wseq.nth_of_seq
added
theorem
wseq.nth_tail
added
theorem
wseq.nth_terminates_le
added
def
wseq.of_list
added
def
wseq.of_list_cons
added
def
wseq.of_list_nil
added
def
wseq.of_mem_append
added
def
wseq.of_seq
added
def
wseq.of_stream
added
def
wseq.productive
added
theorem
wseq.productive_congr
added
def
wseq.remove_nth
added
def
wseq.ret
added
theorem
wseq.ret_bind
added
def
wseq.scanl
added
theorem
wseq.seq_destruct_cons
added
theorem
wseq.seq_destruct_nil
added
theorem
wseq.seq_destruct_think
added
def
wseq.split_at
added
def
wseq.tail.aux
added
def
wseq.tail
added
theorem
wseq.tail_congr
added
theorem
wseq.tail_cons
added
theorem
wseq.tail_nil
added
theorem
wseq.tail_of_seq
added
theorem
wseq.tail_think
added
def
wseq.take
added
def
wseq.think
added
theorem
wseq.think_append
added
theorem
wseq.think_congr
added
theorem
wseq.think_equiv
added
def
wseq.to_list'_cons
added
def
wseq.to_list'_map
added
def
wseq.to_list'_nil
added
def
wseq.to_list'_think
added
def
wseq.to_list
added
def
wseq.to_list_cons
added
def
wseq.to_list_nil
added
theorem
wseq.to_list_of_list
added
def
wseq.to_seq
added
theorem
wseq.to_seq_of_seq
added
def
wseq.union
added
def
wseq.update_nth
added
def
wseq.zip
added
def
wseq.zip_with
added
def
wseq
Created
data/set/basic.lean
added
theorem
set.empty_inter
added
theorem
set.empty_subset
added
theorem
set.empty_union
added
theorem
set.eq_empty_of_forall_not_mem
added
theorem
set.eq_empty_of_subset_empty
added
theorem
set.eq_of_subset_of_subset
added
theorem
set.ext
added
theorem
set.inter_assoc
added
theorem
set.inter_comm
added
theorem
set.inter_empty
added
theorem
set.inter_self
added
theorem
set.mem_empty_eq
added
theorem
set.mem_of_subset_of_mem
added
theorem
set.ne_empty_of_mem
added
theorem
set.not_mem_empty
added
theorem
set.subset.antisymm
added
theorem
set.subset.refl
added
theorem
set.subset.trans
added
theorem
set.union_assoc
added
theorem
set.union_comm
added
theorem
set.union_empty
added
theorem
set.union_self
Created
data/set/default.lean
Created
data/set/finite.lean
added
inductive
set.finite
added
theorem
set.finite_image
added
theorem
set.finite_insert
added
theorem
set.finite_sUnion
added
theorem
set.finite_singleton
added
theorem
set.finite_subset
added
theorem
set.finite_union
Created
data/set/lattice.lean
added
def
set.Inter
added
theorem
set.Inter_eq_comp_Union_comp
added
theorem
set.Inter_eq_sInter_image
added
def
set.Union
added
theorem
set.Union_eq_comp_Inter_comp
added
theorem
set.Union_eq_sUnion_image
added
theorem
set.Union_subset
added
theorem
set.Union_subset_iff
added
theorem
set.bInter_empty
added
theorem
set.bInter_insert
added
theorem
set.bInter_pair
added
theorem
set.bInter_singleton
added
theorem
set.bInter_subset_of_mem
added
theorem
set.bInter_union
added
theorem
set.bInter_univ
added
theorem
set.bUnion_empty
added
theorem
set.bUnion_insert
added
theorem
set.bUnion_pair
added
theorem
set.bUnion_singleton
added
theorem
set.bUnion_subset
added
theorem
set.bUnion_union
added
theorem
set.bUnion_univ
added
theorem
set.bounded_forall_empty_iff
added
theorem
set.bounded_forall_image_iff
added
theorem
set.bounded_forall_image_of_bounded_forall
added
theorem
set.bounded_forall_insert_iff
added
theorem
set.compl_Inter
added
theorem
set.compl_Union
added
theorem
set.compl_comp_compl
added
theorem
set.compl_compl
added
theorem
set.compl_compl_image
added
theorem
set.compl_empty
added
theorem
set.compl_eq_univ_diff
added
theorem
set.compl_inter
added
theorem
set.compl_inter_self
added
theorem
set.compl_sInter
added
theorem
set.compl_sUnion
added
theorem
set.compl_union
added
theorem
set.compl_union_self
added
theorem
set.compl_univ
added
theorem
set.diff_eq
added
theorem
set.diff_subset
added
def
set.disjoint
added
theorem
set.disjoint_bot_left
added
theorem
set.disjoint_bot_right
added
theorem
set.disjoint_symm
added
theorem
set.empty_ne_univ
added
theorem
set.eq_of_mem_singleton
added
def
set.eq_on
added
theorem
set.eq_or_mem_of_mem_insert
added
theorem
set.eq_sep_of_subset
added
theorem
set.eq_univ_of_forall
added
theorem
set.eq_univ_of_univ_subset
added
theorem
set.eq_vimage_subtype_val_iff
added
theorem
set.exists_mem_of_ne_empty
added
theorem
set.fix_set_compl
added
theorem
set.forall_insert_of_forall
added
theorem
set.forall_not_of_sep_empty
added
theorem
set.forall_of_forall_insert
added
theorem
set.image_comp
added
theorem
set.image_empty
added
theorem
set.image_eq_image_of_eq_on
added
theorem
set.image_id
added
theorem
set.image_insert_eq
added
theorem
set.image_subset
added
theorem
set.image_subset_iff_subset_vimage
added
theorem
set.image_union
added
theorem
set.insert_comm
added
theorem
set.insert_def
added
theorem
set.insert_eq
added
theorem
set.insert_eq_of_mem
added
theorem
set.insert_ne_empty
added
theorem
set.insert_of_has_insert
added
theorem
set.insert_sdiff_singleton
added
theorem
set.inter_compl_self
added
theorem
set.inter_def
added
theorem
set.inter_distrib_Union_left
added
theorem
set.inter_distrib_left
added
theorem
set.inter_distrib_right
added
theorem
set.inter_empty_of_inter_sUnion_empty
added
theorem
set.inter_eq_compl_compl_union_compl
added
theorem
set.inter_eq_self_of_subset_left
added
theorem
set.inter_eq_self_of_subset_right
added
theorem
set.inter_left_comm
added
theorem
set.inter_right_comm
added
theorem
set.inter_subset_inter
added
theorem
set.inter_subset_inter_left
added
theorem
set.inter_subset_inter_right
added
theorem
set.inter_subset_left
added
theorem
set.inter_subset_right
added
theorem
set.inter_univ
added
theorem
set.mem_Inter
added
theorem
set.mem_Inter_eq
added
theorem
set.mem_Union_eq
added
theorem
set.mem_bInter
added
theorem
set.mem_bUnion
added
theorem
set.mem_compl
added
theorem
set.mem_compl_eq
added
theorem
set.mem_compl_iff
added
theorem
set.mem_diff
added
theorem
set.mem_diff_eq
added
theorem
set.mem_diff_iff
added
theorem
set.mem_image
added
theorem
set.mem_image_compl
added
def
set.mem_image_elim
added
def
set.mem_image_elim_on
added
theorem
set.mem_image_eq
added
theorem
set.mem_image_of_mem
added
theorem
set.mem_insert
added
theorem
set.mem_insert_iff
added
theorem
set.mem_insert_of_mem
added
theorem
set.mem_inter
added
theorem
set.mem_inter_eq
added
theorem
set.mem_inter_iff
added
theorem
set.mem_of_mem_diff
added
theorem
set.mem_of_mem_insert_of_ne
added
theorem
set.mem_of_mem_inter_left
added
theorem
set.mem_of_mem_inter_right
added
theorem
set.mem_or_mem_of_mem_union
added
theorem
set.mem_powerset
added
theorem
set.mem_powerset_iff
added
theorem
set.mem_sInter
added
theorem
set.mem_sInter_eq
added
theorem
set.mem_sUnion
added
theorem
set.mem_sUnion_eq
added
theorem
set.mem_sep
added
theorem
set.mem_sep_eq
added
theorem
set.mem_sep_iff
added
theorem
set.mem_set_of
added
theorem
set.mem_set_of_eq
added
theorem
set.mem_singleton