## Stream: new members

### Topic: order of arguments

#### Daan van Gent (Nov 05 2022 at 15:49):

Why is the order of arguments in

theorem sup_le_sup_left (h₁ : a ≤ b) (c) : c ⊔ a ≤ c ⊔ b


hypothesis h first and element c second, while

lemma inf_le_inf_right (a : α) {b c : α} (h : b ≤ c) : b ⊓ a ≤ c ⊓ a


is the other way around?

#### Eric Wieser (Nov 05 2022 at 15:54):

To me those both look backwards!

#### Eric Wieser (Nov 05 2022 at 15:58):

docs#sup_le_sup_right and docs#inf_le_inf_left both look right to me, in contrast

#### Daan van Gent (Nov 05 2022 at 16:02):

I see no difference between those and mine. Both don't agree on the order of element vs hypothesis, or is there some logic I am missing?

#### Andrew Yang (Nov 05 2022 at 16:46):

The order of the hypothesis should match the order of appearances in the statement.

#### Daan van Gent (Nov 05 2022 at 17:01):

What does that mean? The hypothesis h₁ : a ≤ b appears nowhere in the statement  c ⊔ a ≤ c ⊔ b

#### Eric Wieser (Nov 05 2022 at 17:08):

It's more of a heuristic than an algorithm. c ⊔ a ≤ c ⊔ b is natural to think of as a ≤ b with c on the left, so in the arguments c is on the left of the a ≤ b argument.

#### Daan van Gent (Nov 05 2022 at 17:54):

I see, thanks! That's not something I would have guessed. I expected something like data to take precedence over propositions.

#### Yaël Dillies (Nov 05 2022 at 18:40):

Actually you should expect the other way because proof arguments are (usually) not inferrable from the rewrite, while data arguments are.

Last updated: Dec 20 2023 at 11:08 UTC