Theorem Submonoid.mem_iSup_prop

Modification history

2025-10-06 18:32
Mathlib/Algebra/Group/Submonoid/Membership.lean
feat(Algebra/Subgroup/Lattice): `mem_biSup_of_directedOn` (#29990) …
Added Submonoid.mem_iSup_propView on Github →