Can I define assumptions in lean?

Dominik Winecki 0
Viewed 25

I'm just starting out with lean. Can I define define the assumptions of a theorem?

For example, proving that for any integer pair min and max, every number x such that min <= x <= max, that min^2 <= x^2 <= max^2. I can define for all integers, but how can I only solve this when the values of min and max meet a constraint (min <= max)?

lean
1 Answers

I would state this theorem like this

example (min max x : ℤ)(hxm : x ≤ max) (hmx : min ≤ x) : min^2 ≤ x^2 ∧ x^2 ≤ max^2

The fact that min ≤ max follows from the other two assumptions, so you needn't include it as an assumption.

Christopher Hughes0
Related