Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-11 23:22 1dddcf69

View on Github →

doc(*): blurbs galore Document all def, class, and inductive that are reasonably public-facing

Estimated changes

modified def continuous
modified theorem is_open_induced
modified theorem tendsto_nhds
added def cauchy
modified theorem finsupp.comap_domain_apply
modified theorem finsupp.comap_domain_zero
modified theorem finsupp.one_def
modified theorem finsupp.smul_apply
modified def bucket_array.modify
modified def bucket_array.write
modified def hash_map.of_list
modified theorem snum.bit_one
modified theorem prod.fst_swap
modified theorem prod.snd_swap
modified def prod.swap
modified theorem prod.swap_swap
modified def computation.destruct
added theorem computation.eq_thinkN'
added theorem computation.eq_thinkN
modified def computation.equiv
modified theorem computation.get_equiv
added theorem computation.get_mem
deleted def computation.get_mem
modified def computation.orelse
modified theorem computation.orelse_ret
modified theorem computation.orelse_think
modified theorem computation.promises_congr
modified theorem computation.ret_orelse
added theorem seq.corec_eq
deleted def seq.corec_eq
added theorem seq.mem_append_left
deleted def seq.mem_append_left
added theorem seq.of_list_append
deleted def seq.of_list_append
added theorem seq.of_list_cons
deleted def seq.of_list_cons
added theorem seq.of_list_nil
deleted def seq.of_list_nil
added theorem seq.of_mem_append
deleted def seq.of_mem_append
added theorem seq.of_stream_append
added theorem seq.of_stream_cons
deleted def seq.of_stream_cons
modified def seq.omap
modified def wseq.bisim_o
modified def wseq.drop.aux
added theorem wseq.drop.aux_none
deleted def wseq.drop.aux_none
added theorem wseq.join_cons
deleted def wseq.join_cons
added theorem wseq.join_nil
deleted def wseq.join_nil
added theorem wseq.join_think
deleted def wseq.join_think
added theorem wseq.lift_rel.equiv
deleted def wseq.lift_rel.equiv
added theorem wseq.lift_rel.refl
deleted def wseq.lift_rel.refl
added theorem wseq.lift_rel.swap
deleted def wseq.lift_rel.swap
added theorem wseq.lift_rel.swap_lem
added theorem wseq.lift_rel.symm
deleted def wseq.lift_rel.symm
added theorem wseq.lift_rel.trans
deleted def wseq.lift_rel.trans
added theorem wseq.lift_rel_cons
deleted def wseq.lift_rel_cons
added theorem wseq.lift_rel_nil
deleted def wseq.lift_rel_nil
added theorem wseq.lift_rel_o.swap
modified def wseq.lift_rel_o
added theorem wseq.mem_append_left
added theorem wseq.of_list_cons
deleted def wseq.of_list_cons
added theorem wseq.of_list_nil
deleted def wseq.of_list_nil
added theorem wseq.of_mem_append
deleted def wseq.of_mem_append
modified def wseq.tail.aux
added theorem wseq.to_list'_cons
deleted def wseq.to_list'_cons
added theorem wseq.to_list'_map
deleted def wseq.to_list'_map
added theorem wseq.to_list'_nil
deleted def wseq.to_list'_nil
added theorem wseq.to_list'_think
deleted def wseq.to_list'_think
added theorem wseq.to_list_cons
deleted def wseq.to_list_cons
added theorem wseq.to_list_nil
deleted def wseq.to_list_nil
added theorem set.mem_image_elim
deleted def set.mem_image_elim
added theorem set.mem_image_elim_on
modified def set.maps_to
added theorem set.maps_to_univ
deleted theorem set.maps_to_univ_univ
modified def sum.swap
modified def fin2.add
modified def fin2.elim0
modified def fin2.insert_perm
modified def fin2.left
modified def fin2.of_nat'
modified def fin2.opt_of_nat
modified def fin2.remap_left
added def fin2.to_nat
modified theorem int.eq_nat_abs_iff_mul
modified def list_all
modified def option.cons
added theorem option.cons_head_tail
deleted def poly.pow
modified def sum.join
modified def vector3.append
modified theorem vector3.append_add
modified theorem vector3.append_cons
modified theorem vector3.append_insert
modified theorem vector3.append_left
modified theorem vector3.append_nil
modified def vector3.cons
modified def vector3.cons_elim
modified theorem vector3.cons_elim_cons
modified theorem vector3.cons_fs
modified theorem vector3.cons_fz
modified theorem vector3.cons_head_tail
modified theorem vector3.eq_nil
modified def vector3.head
modified def vector3.insert
modified theorem vector3.insert_fs
modified theorem vector3.insert_fz
modified def vector3.nil
modified def vector3.nil_elim
modified def vector3.nth
modified def vector3.of_fn
modified theorem vector3.rec_on_cons
modified theorem vector3.rec_on_nil
modified def vector3.tail
added theorem pell.is_pell_conj
deleted def pell.is_pell_conj
added theorem pell.is_pell_mul
deleted def pell.is_pell_mul
added theorem pell.is_pell_nat
deleted def pell.is_pell_nat
added theorem pell.is_pell_norm
deleted def pell.is_pell_norm
added theorem pell.is_pell_one
deleted def pell.is_pell_one
added theorem pell.is_pell_pell_zd
added theorem pell.n_lt_a_pow
deleted def pell.n_lt_a_pow
modified def pell.pell
added theorem pell.xn_ge_a_pow
deleted def pell.xn_ge_a_pow
added theorem zsqrtd.nonnegg_comm
deleted def zsqrtd.nonnegg_comm
added theorem zsqrtd.nonnegg_neg_pos
added theorem zsqrtd.nonnegg_pos_neg
added theorem is_irrefl.swap
deleted def is_irrefl.swap
added theorem is_irrefl_of_is_asymm
added theorem is_strict_order.swap
added theorem is_trans.swap
deleted def is_trans.swap
added theorem is_trichotomous.swap
modified theorem lattice.Inf_le
modified theorem lattice.le_Sup
modified def directed
modified def directed_on
modified theorem filter.lift_le
modified def filter.tendsto
deleted def upwards
modified theorem cardinal.lt_cof_power
modified def ordinal.typein
modified def Class.Class_to_Cong
modified def Class.Cong_to_Class
modified def Class.Union
modified theorem Class.Union_hom
modified theorem Class.diff_hom
modified theorem Class.empty_hom
modified def Class.fval
modified theorem Class.fval_ex
modified theorem Class.insert_hom
modified theorem Class.inter_hom
modified def Class.iota
modified theorem Class.iota_ex
modified theorem Class.iota_val
modified theorem Class.mem_hom_left
modified theorem Class.mem_hom_right
modified theorem Class.mem_univ
modified theorem Class.of_Set.inj
modified def Class.of_Set
modified def Class.powerset
modified theorem Class.powerset_hom
modified theorem Class.sep_hom
modified theorem Class.subset_hom
modified def Class.to_Set
modified theorem Class.to_Set_of_Set
modified theorem Class.union_hom
modified def Class.univ
modified def Set.Union
modified theorem Set.Union_lem
modified theorem Set.Union_singleton
added theorem Set.choice_is_func
deleted def Set.choice_is_func
added theorem Set.choice_mem
deleted def Set.choice_mem
added theorem Set.choice_mem_aux
deleted def Set.choice_mem_aux
modified def Set.empty
added theorem Set.eq_empty
deleted def Set.eq_empty
added theorem Set.ext
deleted def Set.ext
added theorem Set.ext_iff
deleted def Set.ext_iff
modified def Set.funs
added theorem Set.image.mk
deleted def Set.image.mk
modified def Set.image
modified theorem Set.induction_on
modified def Set.is_func
added theorem Set.map_fval
deleted def Set.map_fval
modified theorem Set.map_is_func
modified theorem Set.map_unique
modified def Set.mem
modified theorem Set.mem_Union
modified theorem Set.mem_diff
added theorem Set.mem_empty
deleted def Set.mem_empty
added theorem Set.mem_funs
deleted def Set.mem_funs
added theorem Set.mem_image
deleted def Set.mem_image
added theorem Set.mem_insert
deleted def Set.mem_insert
modified theorem Set.mem_inter
modified theorem Set.mem_map
modified theorem Set.mem_pair
modified theorem Set.mem_pair_sep
modified theorem Set.mem_powerset
added theorem Set.mem_prod
deleted def Set.mem_prod
modified theorem Set.mem_sep
modified theorem Set.mem_singleton'
modified theorem Set.mem_singleton
modified theorem Set.mem_union
added def Set.mk
added theorem Set.mk_eq
modified def Set.omega
modified theorem Set.omega_succ
modified theorem Set.omega_zero
modified def Set.pair
added theorem Set.pair_inj
deleted def Set.pair_inj
added theorem Set.pair_mem_prod
deleted def Set.pair_mem_prod
modified def Set.pair_sep
modified def Set.powerset
modified def Set.prod
modified theorem Set.regularity
modified theorem Set.singleton_inj
modified theorem Set.subset_iff
modified def Set.to_set
modified def pSet.Union
modified def pSet.arity.equiv
added theorem pSet.definable.eq
deleted def pSet.definable.eq
modified def pSet.definable.eq_mk
modified def pSet.definable.resp
modified inductive pSet.definable
modified def pSet.embed
added theorem pSet.equiv.eq
deleted def pSet.equiv.eq
added theorem pSet.equiv.euc
deleted def pSet.equiv.euc
added theorem pSet.equiv.ext
deleted def pSet.equiv.ext
added theorem pSet.equiv.refl
deleted def pSet.equiv.refl
added theorem pSet.equiv.symm
deleted def pSet.equiv.symm
added theorem pSet.equiv.trans
deleted def pSet.equiv.trans
modified def pSet.equiv
modified def pSet.func
modified def pSet.image
added theorem pSet.lift_mem_embed
deleted def pSet.lift_mem_embed
added theorem pSet.mem.congr_left
deleted def pSet.mem.congr_left
added theorem pSet.mem.congr_right
added theorem pSet.mem.ext
deleted def pSet.mem.ext
added theorem pSet.mem.mk
deleted def pSet.mem.mk
modified def pSet.mem
modified theorem pSet.mem_Union
added theorem pSet.mem_empty
deleted def pSet.mem_empty
added theorem pSet.mem_image
deleted def pSet.mem_image
modified theorem pSet.mem_powerset
added theorem pSet.mk_type_func
deleted def pSet.mk_type_func
modified def pSet.of_nat
modified def pSet.omega
modified def pSet.powerset
modified def pSet.resp.equiv
added theorem pSet.resp.euc
deleted def pSet.resp.euc
modified def pSet.resp.eval
modified def pSet.resp.eval_aux
modified def pSet.resp.eval_val
modified def pSet.resp.f
added theorem pSet.resp.refl
deleted def pSet.resp.refl
modified def pSet.resp
added theorem pSet.subset.congr_left
modified def pSet.to_set
modified def pSet.type