Commit 2024-02-04 02:08 c4152bb6

View on Github →

refactor(Set/Countable): redefine Set.Countable (#9831) Redefine Set.Countable s as _root_.Countable s. Fix compile, golf some of the broken proofs.

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/Algebra/AlgebraicCard.lean

Modified Mathlib/Data/Set/Countable.lean

modified theorem Set.Countable.mono

modified theorem Set.Finite.countable

modified theorem Set.countable_coe_iff

added theorem Set.countable_iff_nonempty_encodable

modified theorem Set.to_countable

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Basic.lean

modified theorem Cardinal.le_aleph0_iff_set_countable

Modified Mathlib/Topology/Bases.lean

added theorem TopologicalSpace.isOpen_biUnion_countable

modified theorem TopologicalSpace.secondCountableTopology_of_countable_cover