Commit 2021-11-21 16:46 e0c0d84a

View on Github →

feat(topology/separation): removing a finite set from a dense set preserves density (#10405) Also add the fact that one can find a dense set containing neither top nor bottom in a nontrivial dense linear order.

Estimated changes

Modified src/measure_theory/function/ae_measurable_order.lean

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

added theorem dense.exists_countable_dense_subset_no_bot_top

added theorem exists_countable_dense_no_bot_top

Modified src/topology/bases.lean

Modified src/topology/basic.lean

Modified src/topology/instances/ennreal.lean

added theorem ennreal.exists_countable_dense_no_zero_top

Modified src/topology/separation.lean

added theorem dense.diff_finite

added theorem dense.diff_finset

added theorem dense.diff_singleton

modified theorem finite.is_closed