Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-25 19:35 8da80f4e

View on Github →

feat(data/set/countable): add iff versions of some lemmas (#15671)

Estimated changes

Modified src/data/set/countable.lean

deleted theorem set.countable.bUnion

added theorem set.countable.bUnion_iff

deleted theorem set.countable.sUnion

added theorem set.countable.sUnion_iff

modified theorem set.countable.union

deleted theorem set.countable_Union_Prop

added theorem set.countable_Union_iff

Modified src/measure_theory/constructions/borel_space.lean