## Stream: general

### Topic: Sup of rats

#### 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.

#### 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

#### 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?

#### Kevin Buzzard (Oct 05 2019 at 10:07):

The sum of the reciprocals

Last updated: May 14 2021 at 07:19 UTC