Theorem SetLike.exists_not_mem_of_ne_top

Modification history

2026-02-01 18:45
Mathlib/Data/SetLike/Basic.lean
refactor: remove order instances from `SetLike` (#32984) …
Modified SetLike.exists_not_mem_of_ne_topView on Github →
2025-11-06 15:01
Mathlib/Data/SetLike/Basic.lean
feat(SetLike): add exists_not_mem_of_ne_top lemma (#30946) …
Added SetLike.exists_not_mem_of_ne_topView on Github →