Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.finite.exists_maximal_wrt

Modification history

2020-02-05 06:25
src/data/set/finite.lean
refactor(*): migrate from `≠ ∅` to `set.nonempty` (#1954) …
Modified set.finite.exists_maximal_wrtView on Github →
2019-03-05 09:21
src/data/set/finite.lean
feat(data/set): add exists_maximal_wrt
Added set.finite.exists_maximal_wrtView on Github →