mathlib

12ad63e6 - feat(order/conditionally_complete_lattice): Map `Inf` by monotone function (#14118)