Theorem isGLB_image2_of_isLUB_isLUB

Modification history

2026-04-11 09:33
Mathlib/Order/GaloisConnection/Basic.lean
chore(Order/GaloisConnection/Basic): use `to_dual` (#37885) …
Deleted isGLB_image2_of_isLUB_isLUBView on Github →
2026-01-28 14:02
Mathlib/Order/GaloisConnection/Basic.lean
feat: IsLUB versions of [c]sSup_image2_eq_[c]sSup_[c]sSup (#34104) …
Added isGLB_image2_of_isLUB_isLUBView on Github →