Theorem Subgroup.mem_biSup_of_directedOn

Modification history

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