Zulip Chat Archive
Stream: mathlib4
Topic: Minimum of a finite set
Martin Dvořák (Oct 06 2023 at 14:35):
How can I get a minimum of a finite non-empty set?
Ideally in the following settings (but any notion of minimum of a set would be OK):
import Mathlib.Data.Fintype.Basic
example {A B : Type} [Fintype A] [Inhabited A] [LinearOrder B] (f : A → B) : B := sorry
I would like to know the least value in the range of f.
Ruben Van de Velde (Oct 06 2023 at 14:38):
Does docs#Finset.min' apply?
Yaël Dillies (Oct 06 2023 at 14:39):
Notification Bot (Oct 06 2023 at 17:41):
Geoffrey Irving has marked this topic as resolved.
Geoffrey Irving (Oct 06 2023 at 17:42):
Oops, misclick. I’m surprised I have the ability to do that.
Kevin Buzzard (Oct 06 2023 at 17:42):
We'd love it if nobody has that ability, but we can't figure out how to turn it off (and we've tried).
Notification Bot (Oct 07 2023 at 21:22):
Yongyi Chen has marked this topic as unresolved.
Notification Bot (Oct 07 2023 at 21:22):
Yongyi Chen has marked this topic as resolved.
Yongyi Chen (Oct 07 2023 at 21:23):
Apparently I have the ability to not only resolve but also resolve a topic. Although I resolved it again since this looks resolved...
Martin Dvořák (Oct 07 2023 at 21:25):
It isn't resolved for me yet. I just decided to continue next week, as the minimum was giving me too much trouble on Friday.
Notification Bot (Oct 07 2023 at 23:16):
Yongyi Chen has marked this topic as unresolved.
Yongyi Chen (Oct 07 2023 at 23:16):
OK. Pretend I did nothing.
Last updated: Dec 20 2023 at 11:08 UTC