Theorem GaloisConnection.u_l_top

Modification history

2025-01-20 11:09
Mathlib/Order/GaloisConnection/Basic.lean
chore(Order): split `GaloisConnection` into `Defs.lean` and `Basic.lean` (#20798) …
Modified GaloisConnection.u_l_topView on Github →
2025-01-01 21:51
Mathlib/Order/GaloisConnection.lean
feat: add `Set.preimage_image_univ` and associated `GaloisConnection` result (#20346) …
Added GaloisConnection.u_l_topView on Github →