Commit 2022-11-07 03:20 4a38f249

View on Github →

chore(data/set/basic): Make set.nonempty.ne_empty an alias (#17382) Make nonempty.ne_empty an alias of ne_empty_iff_nonempty and remove empty_not_nonempty in favor of not_nonempty_empty.

Estimated changes

Modified src/analysis/convex/exposed.lean

Modified src/data/set/basic.lean

deleted theorem set.empty_not_nonempty

deleted theorem set.nonempty.ne_empty

modified theorem set.not_nonempty_empty

Modified src/data/set/finite.lean

Modified src/measure_theory/measure/outer_measure.lean

Modified src/order/filter/bases.lean

Modified src/order/filter/basic.lean