Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-11 11:32 28b46a21

View on Github →

fix(data/set/countable): finish proof countable_sUnion

Estimated changes

Modified data/set/countable.lean

deleted theorem option.bind_some

modified theorem set.countable_sUnion

deleted def set.enumerate

deleted theorem set.enumerate_eq_none

deleted theorem set.enumerate_eq_none_of_sel

deleted theorem set.enumerate_inj

deleted theorem set.enumerate_mem

Created data/set/enumerate.lean

added theorem option.bind_some

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