Massot Exercise 0080

Stream: Berkeley Lean Seminar

[Jordan Brown]

I have been stuck trying to figure out how to prove that the range of a continuous function on a compact interval is bounded, as after I form the set that is the range and try to show the inclusion, taking say y to be an arbitrary element of the range, I cannot get some x in the interval such that y = f x, when it seems like this should be definitionally true. The solution uses rintros, but whenever I try to use it, I get an error saying that the range is not an inductive datatype. How can I get around this?

[Kyle Miller]

Could you post your code? (Make sure to put it between ``` marks.) You might also consider posting it, with code, in the "new members" stream.

[Kyle Miller]

In my own solution, I did intros y yel first, then I did rcases on yel to split it up. I'd need to see how you defined the range to be sure, though.

[Patrick Lutz]

I did more or less the same thing as Kyle. I defined A := { y | ∃ x ∈ Icc a b, f x = y } and then to prove A ⊆ Icc c d I first used intros y hy and then rcases hy with ⟨x, x_in, hx⟩ One thing to keep in mind is that in Lean, A ⊆ Icc c d is basically synonymous with something like ∀ (y : ℝ) (hy : y ∈ A), y ∈ Icc c d That is, an element of a subset should really be thought of as a pair consisting of an element of the set (in this case $\R$) and a proof that the element is in the subset. So to prove A ⊆ Icc c d you need to give a proof which takes an element of $\R$ and a proof that that element is in $A$ and produce a proof that the element is also in $[c, d]$.

[Patrick Lutz]

Also, I second Kyle in saying it could be useful to post your code

[Patrick Lutz]

It might be especially useful to post how you defined the range of $f$ on the interval

[Jordan Brown]

Hm, this is basically what I was trying to do and it keeps giving me the error "rcases tactic failed: y_in : [anonymous] is not an inductive datatype". The code currently is:

begin
  have alpha:={x|∃ y ∈ Icc a b, f y = x},
  cases bdd_above_segment hf with u v,
  cases bdd_below_segment hf with c d,
  have z: ∃ x∈ Icc c u,is_sup alpha x,
  have g: a∈ Icc a b,
  exact ⟨ le_refl a,hab⟩ ,
  have h: alpha ⊆ Icc u c,
  intros y y_in,
  rcases y_in with ⟨x,x_in, hx⟩,


end '''

[Kevin Buzzard]

that first have should be a let.

[Kevin Buzzard]

You used have so Lean instantly forgot the definition of alpha and only remembered its type, like with proofs you remember what it's a proof of, but don't remember what the proof is.

[Jordan Brown]

Ah, that fixed it immediately! I did not realize there was a difference. Thanks!

[Kevin Buzzard]

Let for Type, have for Prop

[Patrick Lutz]

Also worth mentioning that set is sometimes useful. It's like let but gives you direct access to a proof that the new variable is equal to the expression used to define it. E.g. let x := f n vs. set x := f n with hx. In the latter, hx is a proof of the proposition x = f n which is useful because otherwise some tactics (like linarith) can't see this fact