Theorem Finite.map_iSup_of_monotoneOn

Modification history

2026-03-03 11:03

Mathlib/Data/Fintype/Order.lean

feat(Data/Fintype/Order): add API for ciSup with finite indexing type (#35260) …

Added Finite.map_iSup_of_monotoneOn View on Github →