Theorem Finset.Nonempty.sup'_eq_cSup_image

Modification history

2024-01-17 13:26

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

chore(Order/ConditionallyCompleteLattice/Finset): merge duplicate lemmas (#9807)

Deleted Finset.Nonempty.sup'_eq_cSup_image View on Github →

2023-01-21 16:46

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

feat: port Order.ConditionallyCompleteLattice.Finset (#1748)

Added Finset.Nonempty.sup'_eq_cSup_image View on Github →