Theorem Submonoid.mem_biSup_of_directedOn

Modification history

2026-05-05 10:37
Mathlib/Algebra/Group/Submonoid/Membership.lean
feat(Order/Directed): directedness under composition by a surjective function (#38861) …
Modified Submonoid.mem_biSup_of_directedOnView on Github →
2025-10-06 18:32
Mathlib/Algebra/Group/Submonoid/Membership.lean
feat(Algebra/Subgroup/Lattice): `mem_biSup_of_directedOn` (#29990) …
Added Submonoid.mem_biSup_of_directedOnView on Github →