Mathlib v3 is deprecated. Go to Mathlib v4

Theorem cInf_image2_eq_cSup_cSup

Modification history

2022-06-14 13:35
src/order/conditionally_complete_lattice.lean
feat(order/{conditionally_complete_lattice,galois_connection): Supremum of `set.image2` (#14307) …
Added cInf_image2_eq_cSup_cSupView on Github →