Mathlib Changelog
Changelog
About
Github
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