Commit 2021-05-14 04:49 3124e1d1
View on Github →feat(data/finset/lattice): choice-free le_sup_iff and lt_sup_iff (#7584)
Propagate to finset the change to le_sup_iff [is_total α (≤)] and lt_sup_iff [is_total α (≤)] made in #7455.
feat(data/finset/lattice): choice-free le_sup_iff and lt_sup_iff (#7584)
Propagate to finset the change to le_sup_iff [is_total α (≤)] and lt_sup_iff [is_total α (≤)] made in #7455.