Theorem isLUB_image2_of_isGLB_isLUB

Modification history

2026-01-28 14:02
Mathlib/Order/GaloisConnection/Basic.lean
feat: IsLUB versions of [c]sSup_image2_eq_[c]sSup_[c]sSup (#34104) …
Added isLUB_image2_of_isGLB_isLUBView on Github →