Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 18:31 12e5f2e0

View on Github →

refactor(data/set/countable): make set.countable protected (#14886) I'm going to add _root_.countable typeclass, a data-free version of encodable.

Estimated changes

modified theorem not_countable_complex
modified theorem cardinal.not_countable_real
modified theorem set.countable.image2
modified theorem set.countable.image
modified theorem set.countable.insert
modified theorem set.countable.mono
modified theorem set.countable.sUnion
deleted def set.countable
modified theorem set.countable_Union
modified theorem set.countable_Union_Prop
modified theorem set.countable_empty
modified theorem set.countable_encodable'
modified theorem set.countable_encodable
modified theorem set.countable_insert
modified theorem set.countable_is_bot
modified theorem set.countable_is_top
modified theorem set.countable_pi
modified theorem set.countable_range
modified theorem set.countable_singleton
modified theorem set.countable_union
modified theorem set.finite.countable
modified theorem set.subset_range_enumerate
modified theorem set.subsingleton.countable
modified theorem ae_measurable_binfi
modified theorem ae_measurable_bsupr
modified theorem measurable_binfi
modified theorem measurable_bsupr
modified theorem measurable_set.pi
modified theorem measurable_set_pi
modified theorem measurable_set.bInter
modified theorem measurable_set.bUnion
modified theorem measurable_set.sInter
modified theorem measurable_set.sUnion
modified theorem measure_theory.ae_ball_iff
modified theorem countable_bInter_mem
modified theorem countable_sInter_mem
modified theorem eventually_countable_ball
modified theorem cardinal.mk_set_le_aleph_0
modified theorem is_Gδ_bInter
modified theorem is_Gδ_bInter_of_open
modified theorem is_Gδ_sInter
modified theorem set.countable.is_Gδ_compl
modified theorem set.countable.is_separable
modified theorem dense_sInter_of_Gδ
modified theorem dense_sInter_of_open
modified theorem dimH_bUnion
modified theorem dimH_countable
modified theorem dimH_sUnion