Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-17 04:23 e017f0f1

View on Github →

feat(data/computability): primrec, denumerable

Estimated changes

Modified analysis/limits.lean

Modified analysis/topology/infinite_sum.lean

Modified analysis/topology/topological_space.lean

added theorem topological_space.Union_basis_of_is_open

added theorem topological_space.sUnion_basis_of_is_open

Modified data/bool.lean

modified theorem bool.cond_ff

added theorem bool.cond_to_bool

modified theorem bool.cond_tt

added theorem bool.to_bool_and

added theorem bool.to_bool_not

added theorem bool.to_bool_or

Created data/computability/primrec.lean

added def nat.cases

added theorem nat.cases_succ

added theorem nat.cases_zero

added def nat.elim

added theorem nat.elim_succ

added theorem nat.elim_zero

added theorem nat.primrec.add

added theorem nat.primrec.cases1

added theorem nat.primrec.cases

added theorem nat.primrec.const

added theorem nat.primrec.mul

added theorem nat.primrec.of_eq

added theorem nat.primrec.pow

added theorem nat.primrec.prec1

added theorem nat.primrec.pred

added theorem nat.primrec.sub

added theorem nat.primrec.swap'

added inductive nat.primrec

added def nat.unpaired

added def primcodable.of_equiv

added theorem primrec.bind_decode_iff

added theorem primrec.comp

added theorem primrec.comp₂

added theorem primrec.cond

added theorem primrec.const

added theorem primrec.dom_bool

added theorem primrec.dom_bool₂

added theorem primrec.dom_denumerable

added theorem primrec.dom_fintype

added theorem primrec.encdec

added theorem primrec.encode_iff

added theorem primrec.fst

added theorem primrec.ite

added theorem primrec.list_find_index

added theorem primrec.list_index_of

added theorem primrec.list_inth

added theorem primrec.list_nth

added theorem primrec.map_decode_iff

added theorem primrec.nat_add

added theorem primrec.nat_bit0

added theorem primrec.nat_bit1

added theorem primrec.nat_bit

added theorem primrec.nat_bodd

added theorem primrec.nat_bodd_div2

added theorem primrec.nat_cases'

added theorem primrec.nat_cases1

added theorem primrec.nat_cases

added theorem primrec.nat_div2

added theorem primrec.nat_div

added theorem primrec.nat_div_mod

added theorem primrec.nat_elim'

added theorem primrec.nat_elim1

added theorem primrec.nat_elim

added theorem primrec.nat_iff

added theorem primrec.nat_le

added theorem primrec.nat_mod

added theorem primrec.nat_mul

added theorem primrec.nat_sub

added theorem primrec.of_eq

added theorem primrec.of_nat_iff

added theorem primrec.option_bind1

added theorem primrec.option_bind

added theorem primrec.option_cases

added theorem primrec.option_iget

added theorem primrec.option_map1

added theorem primrec.option_map

added theorem primrec.option_some

added theorem primrec.option_some_iff

added theorem primrec.pair

added theorem primrec.pred

added theorem primrec.snd

added theorem primrec.succ

added theorem primrec.unpair

added def primrec

added theorem primrec_pred.comp

added theorem primrec_pred.of_eq

added def primrec_pred

added theorem primrec_rel.comp

added theorem primrec_rel.comp₂

added theorem primrec_rel.of_eq

added def primrec_rel

added theorem primrec₂.comp

added theorem primrec₂.comp₂

added theorem primrec₂.const

added theorem primrec₂.curry

added theorem primrec₂.encode_iff

added theorem primrec₂.left

added theorem primrec₂.mkpair

added theorem primrec₂.nat_iff'

added theorem primrec₂.nat_iff

added theorem primrec₂.of_eq

added theorem primrec₂.of_nat_iff

added theorem primrec₂.option_some_iff

added theorem primrec₂.right

added theorem primrec₂.swap

added theorem primrec₂.uncurry

added theorem primrec₂.unpaired'

added theorem primrec₂.unpaired

added def primrec₂

Created data/denumerable.lean

added theorem denumerable.decode_eq_of_nat

added theorem denumerable.decode_is_some

added theorem denumerable.denumerable_list_aux

added theorem denumerable.encode_of_nat

added def denumerable.equiv₂

added def denumerable.eqv

added def denumerable.lower'

added def denumerable.lower

added theorem denumerable.lower_raise'

added theorem denumerable.lower_raise

added def denumerable.mk'

added def denumerable.of_equiv

added theorem denumerable.of_equiv_of_nat

added def denumerable.of_nat

added theorem denumerable.of_nat_encode

added theorem denumerable.of_nat_nat

added theorem denumerable.of_nat_of_decode

added def denumerable.pair

added theorem denumerable.prod_nat_of_nat

added theorem denumerable.prod_of_nat_val

added def denumerable.raise'

added theorem denumerable.raise'_chain

added def denumerable.raise'_finset

added theorem denumerable.raise'_sorted

added def denumerable.raise

added theorem denumerable.raise_chain

added theorem denumerable.raise_lower'

added theorem denumerable.raise_lower

added theorem denumerable.raise_sorted

added theorem denumerable.sigma_of_nat_val

Modified data/encodable.lean

added def encodable.decidable_eq_of_encodable

added theorem encodable.decode_ge_two

added def encodable.decode_list

added def encodable.decode_multiset

added theorem encodable.decode_of_equiv

added theorem encodable.decode_one

added theorem encodable.decode_option_succ

added theorem encodable.decode_option_zero

added theorem encodable.decode_prod_val

added def encodable.decode_sigma

added theorem encodable.decode_sigma_val

added def encodable.decode_subtype

added def encodable.decode_sum

added theorem encodable.decode_unit_succ

added theorem encodable.decode_unit_zero

added theorem encodable.decode_zero

added def encodable.encodable_of_list

added theorem encodable.encode_ff

added theorem encodable.encode_injective

added def encodable.encode_list

added def encodable.encode_multiset

added theorem encodable.encode_none

added theorem encodable.encode_of_equiv

added theorem encodable.encode_prod_val

added def encodable.encode_sigma

added theorem encodable.encode_sigma_val

added theorem encodable.encode_some

added theorem encodable.encode_star

added def encodable.encode_subtype

added def encodable.encode_sum

added theorem encodable.encode_tt

added def encodable.of_equiv

added def encodable.of_left_injection

added def encodable.of_left_inverse

added def encodable.trunc_encodable_of_fintype

deleted def encodable_of_equiv

deleted def encodable_of_left_injection

deleted def encodable_of_list

deleted theorem encode_injective

deleted def trunc_encodable_of_fintype

Modified data/equiv.lean

added theorem equiv.symm_symm

Modified data/finset.lean

added theorem finset.attach_map_val

added def finset.map

added theorem finset.map_empty

added theorem finset.map_eq_empty

added theorem finset.map_eq_image

added theorem finset.map_filter

added theorem finset.map_insert

added theorem finset.map_inter

added theorem finset.map_map

added theorem finset.map_refl

added theorem finset.map_singleton

added theorem finset.map_subset_map

added theorem finset.map_to_finset

added theorem finset.map_union

added theorem finset.map_val

added theorem finset.mem_map

added theorem finset.mem_map_of_mem

added theorem finset.sort_sorted_lt

Modified data/fintype.lean

added theorem fintype.exists_univ_list

Modified data/list/basic.lean

added theorem list.filter_congr

added theorem list.foldl_ext

added theorem list.foldr_ext

added theorem list.map_add_range'

added theorem list.nth_le_map'

added theorem list.nth_le_map

added theorem list.nth_map

added theorem list.pairwise.and

added theorem list.pairwise.imp₂

added theorem list.range'_eq_map_range

added theorem list.range_succ_eq_map

added theorem list.reverse_range'

Modified data/list/sort.lean

modified theorem list.eq_of_sorted_of_perm

added theorem list.merge_sort_eq_self

Modified data/multiset.lean

Modified data/nat/basic.lean

Modified data/nat/pairing.lean

modified theorem nat.mkpair_unpair

modified theorem nat.unpair_mkpair

Modified data/option.lean

added theorem option.map_none'

added theorem option.map_some'

Modified data/rat.lean

Modified data/semiquot.lean

added theorem semiquot.is_pure.min

added theorem semiquot.is_pure.mono

added theorem semiquot.is_pure_iff

added theorem semiquot.pure_inj

Modified data/seq/parallel.lean

Modified data/seq/seq.lean

Modified data/seq/wseq.lean

Modified data/set/countable.lean

Modified logic/basic.lean

added theorem and.right_comm

added theorem and.rotate

Modified logic/embedding.lean

added def function.embedding.subtype

Modified order/basic.lean