Commit 2022-06-28 00:05 ee7f38c7

View on Github →

chore(data/set/basic): remove duplicate nonempty_insert in favor of insert_nonempty (#14884) This name matches e.g. univ_nonempty and singleton_nonempty.

Estimated changes

Modified src/data/set/basic.lean

modified theorem set.insert_nonempty

deleted theorem set.nonempty_insert

Modified src/order/conditionally_complete_lattice.lean

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