basic): deduplicate (#16287)

Commit

3 years ago

chore(topology/algebra/order/basic): deduplicate (#16287) Primed and non-primed versions of 2 lemmas were almost defeq. Merge them.

Author

urkud

Parents