Zulip Chat Archive

Stream: general

Topic: Sup of rats


view this post on Zulip Johan Commelin (Oct 05 2019 at 04:14):

Do we want some form of supremum for sets of rational numbers? Of course there is always the hassle with the empty set.
What is the cleanest way to state the following problem in Lean:

lemma forty_two (a b c : ) (h : (0:) < 1 - (1/a + 1/b + 1/c)) :
  (1:)/(1 - (1/a + 1/b + 1/c))  42 :=
begin
end

I want to claim that the 42 is the upper bound and that it is strict.

view this post on Zulip Johan Commelin (Oct 05 2019 at 08:15):

For the record, the relevant generalisation to more than 3 nats seems to be discussed in https://www.jstor.org/stable/2299023

view this post on Zulip Kevin Buzzard (Oct 05 2019 at 10:07):

Why not just say that if it's less than 1 then it's le 41/42?

view this post on Zulip Kevin Buzzard (Oct 05 2019 at 10:07):

The sum of the reciprocals


Last updated: May 14 2021 at 07:19 UTC