Yiming Xu (Jan 31 2025 at 15:24): Yiming Xu (Jan 31 2025 at 15:24):There seems different constants that allows one to take out the minimal value from a set. I discovered Inf first, but by searching:
find_theorems "Inf" "_ :: nat"
I found something called LEAST as well.
Conditionally_Complete_Lattices.Inf_nat_def: Inf ?X = (LEAST n. n ∈ ?X)
a further search using
find_theorems " (LEAST _. _)"
leads me to Least:
Orderings.ord_class.Least_def: Least ?P = (THE x. ?P x ∧ (∀y. ?P y ⟶ x ≤ y))
There is also a Min, but only works for finite sets if I understand correctly.
May I please ask what should I know which one to use? I made a definition using Inf. The motivation for me to ask it is I do not want to miss any useful theorems and do not want sledgehammer to hate it.
Yiming Xu (Jan 31 2025 at 15:25):In particular, could someone please tell me which theorem is the most helpful when proving "Inf X = something"? This one:
Orderings.order_class.Least_equality:
?P ?x ⟹ (⋀y. ?P y ⟹ ?x ≤ y) ⟹ Least ?P = ?x
seems best to me, but I wonder if there are other useful things that I do not know.
Mathias Fleury (Jan 31 2025 at 15:54):Min for finite sets
Inf for (possibly) infinite sets.
Yiming Xu (Jan 31 2025 at 15:55):Yes, this is the reason I know I should not use Min. If nothing further special to know, then I will just remember this single thing.
Mathias Fleury (Jan 31 2025 at 15:56):Yiming Xu said:
In particular, could someone please tell me which theorem is the most helpful when proving "Inf X = something"? This one:
Orderings.order_class.Least_equality:
?P ?x ⟹ (⋀y. ?P y ⟹ ?x ≤ y) ⟹ Least ?P = ?x
seems best to me, but I wonder if there are other useful things that I do not know.
This theorems means that the set is finite once you have an upper bound and the lower bound is included in the set
Mathias Fleury (Jan 31 2025 at 15:56):The hard part is on stuff like Inf {x \in Q. x > sqrt(2)}
Mathias Fleury (Jan 31 2025 at 15:56):where the Inf is actually sqrt(2) and not in the set
Yiming Xu (Jan 31 2025 at 15:57):Sorry, how does the theorem tell about upper bound? I cannot see anything relevant to the upper bound.
Mathias Fleury (Jan 31 2025 at 16:02):Mathias Fleury said:
Yiming Xu said:
In particular, could someone please tell me which theorem is the most helpful when proving "Inf X = something"? This one:
Orderings.order_class.Least_equality:
?P ?x ⟹ (⋀y. ?P y ⟹ ?x ≤ y) ⟹ Least ?P = ?x
seems best to me, but I wonder if there are other useful things that I do not know.This theorems means that the set is finite once you have an upper bound and the lower bound is included in the set
I badly worded this and it is actually wrong. I meant that the set is "closed" which makes some things easier to say and to reason on
Mathias Fleury (Jan 31 2025 at 16:03):(I was thinking of natural numbers and in this cases, the set becomes finite because it is bound by any element in the set)
Yiming Xu (Jan 31 2025 at 16:04):I conceive it as a warning that the Inf may not be in the set. (Thankfull it would not happen on the natural numbers).
Last updated: Mar 08 2025 at 01:11 UTC