Theorem directedOn_onFun_iff

Modification history

2025-10-06 18:32
Mathlib/Order/Directed.lean
feat(Algebra/Subgroup/Lattice): `mem_biSup_of_directedOn` (#29990) …
Added directedOn_onFun_iffView on Github →