Commit 2023-01-24 06:27 83bdaed2

View on Github →

Feat: port Data.Set.Countable (#1788)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Countable/Defs.lean

Created Mathlib/Data/Set/Countable.lean

added theorem Finset.countable_to_set

added theorem Set.Countable.bunionᵢ_iff

added theorem Set.Countable.exists_eq_range

added theorem Set.Countable.image2

added theorem Set.Countable.image

added theorem Set.Countable.insert

added theorem Set.Countable.mono

added theorem Set.Countable.of_subsingleton

added theorem Set.Countable.preimage_of_injOn

added theorem Set.Countable.union

added theorem Set.Countable.unionₛ_iff

added theorem Set.Finite.countable

added theorem Set.MapsTo.countable_of_injOn

added theorem Set.Subsingleton.countable

added theorem Set.countable_coe_iff

added theorem Set.countable_empty

added theorem Set.countable_iff_exists_injOn

added theorem Set.countable_iff_exists_subset_range

added theorem Set.countable_insert

added theorem Set.countable_isBot

added theorem Set.countable_isTop

added theorem Set.countable_of_injective_of_countable_image

added theorem Set.countable_pi

added theorem Set.countable_range

added theorem Set.countable_setOf_finite_subset

added theorem Set.countable_singleton

added theorem Set.countable_union

added theorem Set.countable_unionᵢ

added theorem Set.countable_unionᵢ_iff

added theorem Set.countable_univ

added theorem Set.countable_univ_pi

added def Set.enumerateCountable

added theorem Set.exists_seq_cover_iff_countable

added theorem Set.exists_seq_supᵢ_eq_top_iff_countable

added theorem Set.subset_range_enumerate

added theorem Set.to_countable