Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-10 23:28 8ee26290

View on Github →

feat(data/set): add countable sets

Estimated changes

Modified data/encodable.lean

Created data/set/countable.lean

added theorem option.bind_some

added theorem set.countable.to_encodable

added def set.countable

added theorem set.countable_empty

added theorem set.countable_encodable'

added theorem set.countable_encodable

added theorem set.countable_iff_exists_surjective

added theorem set.countable_image

added theorem set.countable_sUnion

added theorem set.countable_singleton

added theorem set.countable_subset

added def set.encodable_of_inj

added def set.enumerate

added theorem set.enumerate_eq_none

added theorem set.enumerate_eq_none_of_sel

added theorem set.enumerate_inj

added theorem set.enumerate_mem

Modified data/set/finite.lean

added def set.infinite

Modified logic/function_inverse.lean

added theorem set.inv_fun_on_eq'

Modified order/filter.lean