Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 09:31 f40cd3cf

View on Github →

feat(topology/algebra/order/basic): in a second-countable linear order, only countably many points are isolated to the right (#14564) This makes it possible to remove a useless densely_ordered assumption in a lemma in borel_space.

Estimated changes

Modified src/data/set/basic.lean

deleted def set.unique_empty

Modified src/data/set/countable.lean

added theorem set.countable.of_subsingleton

Modified src/data/set/finite.lean

added theorem set.finite.of_subsingleton

Modified src/measure_theory/constructions/borel_space.lean

modified theorem measurable_set_of_mem_nhds_within_Ioi

modified theorem measurable_set_of_mem_nhds_within_Ioi_aux

Modified src/measure_theory/integral/set_to_l1.lean

Modified src/topology/algebra/order/basic.lean

added theorem countable_of_isolated_left

added theorem countable_of_isolated_right

added theorem set.pairwise_disjoint.countable_of_Ioo

Modified src/topology/separation.lean

added theorem topological_space.is_topological_basis.exists_mem_of_ne