le/lt trans

Stream: new members

[Iocta]

example : ∀ {a b c : real}, a < b → b ≤ c → a < c :=
begin
intros a b c h1 h2,
end

1) How do I say this without the \forall? 2) What is the name of this lemma?

[Jalex Stark]

import tactic
example (a b c : real) : a < b → b ≤ c → a < c :=
begin
  library_search
end

[Jalex Stark]

putting things to the left of the binder makes them arguments

[Jalex Stark]

in this case, you've stated the lemma in a way that's very similar to how it's stated in the library, so library_search finds the name for you

[Iocta]

Thanks

[Jalex Stark]

it sounds dumb, but it's actually pretty efficient to guess the name of this lemma using autocomplete

[Iocta]

How come I can't

variables {a b c : real}
example  : a < b → b ≤ c : a < c := sorry

[Jalex Stark]

you have two binders

[Jalex Stark]

: is not a synonym for →

[Jalex Stark]

this should work

variables {a b c : real}
example (hab : a < b) (hbc : b ≤ c) : a < c := sorry

[Jalex Stark]

hypotheses to the left of the binder ought to have names, though I think you can omit them

[Iocta]

Ah ok