Theorem GaloisConnection.monotone_l_comp_u

Modification history

2026-03-21 06:41
Mathlib/Order/GaloisConnection/Defs.lean
feat: concept generated by set of objects/attributes (#30001)
Added GaloisConnection.monotone_l_comp_uView on Github →