Commit 2020-05-16 17:50 a7b17cdd
View on Github →feat(data/finset): remove uses of choice for infima (#2699)
This PR removes the dependence of many lemmas about inf of finset sets on the axiom of choice. The motivation for this is to make category_theory.limits.has_finite_limits_of_semilattice_inf_top not depend on choice, which I would like so that I can prove independence results about topos models of set theory from the axiom of choice.
This does make the decidable_classical linter fail.