## Stream: new members

### Topic: Order reversing bijection on fin n

#### Antoine Labelle (Nov 01 2021 at 23:11):

This may be a stupid question, but I was wondering what was the simplest way to denote the element n-1-i given i : fin n. If I just write it as such Lean complains because n is of type nat so it doesn't know how to subtract something from it.
I noticed that Lean accepts ⟨n-1-i, _⟩, but adds n-1-i<n as a new goal. That seems to work but feels too convoluted but something that should be simple.
Is the order-reversing bijection i ↦ n-1-i on fin n already defined somewhere, and if not what is the best way to work with it?

#### Yakov Pechersky (Nov 01 2021 at 23:13):

fin.last n - i

Thanks!

#### Eric Wieser (Nov 01 2021 at 23:22):

Or I think docs#equiv.sub_left (fin.last n) if you want the bijection

#### Antoine Labelle (Nov 01 2021 at 23:43):

equiv.sub_left is protected, can I still use it? Lean gives me an "unknown identifier" message even if I import data.equiv.mul_add.

#### Alex J. Best (Nov 01 2021 at 23:47):

Yes, check out attr#protected, it should still be usable, just you always need to use its full name. If you post a full example we can try and see what's wrong.

#### Antoine Labelle (Nov 01 2021 at 23:57):

Here is my code

import data.finset.sort

open_locale big_operators

theorem imo1994 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)
(hrange : ∀ a ∈ A, a ≥ 1 ∧ a ≤ n) (hadd : ∀ a b ∈ A, a + b ≤ n → a + b ∈ A) :
(n+1)/2 ≤ (∑ x in A, x)/(m+1) :=
begin
have a := finset.order_emb_of_fin A hm,
set flip := equiv.sub_left (fin.last m),
end


#### Alex J. Best (Nov 02 2021 at 00:03):

You also need a newline after the first set of backticks, like so


import blah

lemma foo := trivial



#### Antoine Labelle (Nov 02 2021 at 00:17):

Weird, do you have any idea why it wouldn't work for me in VScode? Could I have problems with my installation of mathlib?

#### Alex J. Best (Nov 02 2021 at 00:19):

Yes, that could be the case, when did you install lean/mathlib? Maybe it just needs an update?

#### Antoine Labelle (Nov 02 2021 at 00:28):

Oh yeah, an upgrade worked :sweat_smile: . Thanks for the help!

Last updated: Dec 20 2023 at 11:08 UTC