## Stream: new members

### Topic: iff with ∃ on both sides

#### Heather Macbeth (Aug 05 2020 at 21:30):

Is there a more efficient way to do this?

import data.equiv.basic

example (A : Type*) (B : Type*) (f : equiv A B) (P : B → Prop) : (∃ a, P (f a)) ↔ (∃ b, P b) :=
begin
split,
{ rintros ⟨a, ha⟩,
use [f a, ha] },
{ rintros ⟨b, hb⟩,
use f.symm b,
simpa using hb }
end


#### Patrick Massot (Aug 05 2020 at 21:38):

tauto can do the first implication.

#### Heather Macbeth (Aug 05 2020 at 21:39):

I was hoping for something that doesn't involve a split ...

#### Patrick Massot (Aug 05 2020 at 21:41):

I was hoping equiv_rw would help, but it doesn't.

#### Yury G. Kudryashov (Aug 05 2020 at 21:41):

There should be a lemma in data.equiv.basic

#### Yury G. Kudryashov (Aug 05 2020 at 21:43):

And there should be a lemma in the namespace function.surjective

#### Yury G. Kudryashov (Aug 05 2020 at 21:44):

Let's try docs#function.surjective.exists

(deleted)

#### Yury G. Kudryashov (Aug 05 2020 at 21:50):

We have docs#equiv.forall_congr but not equiv.exists_congr.

#### Heather Macbeth (Aug 05 2020 at 21:52):

I guess that's ok?

example (A : Type*) (B : Type*) (f : equiv A B) (P : B → Prop) : (∃ b, P b) ↔ (∃ a, P (f a)) :=
function.surjective.exists (equiv.surjective f)


is pretty short!

#### Rob Lewis (Aug 05 2020 at 22:22):

Or even shorter, f.surjective.exists?

Oops, yes!

#### Anatole Dedecker (Aug 05 2020 at 22:38):

Dot notation is awesome

#### Yury G. Kudryashov (Aug 06 2020 at 01:15):

Rob Lewis said:

Or even shorter, f.surjective.exists?

That's why the lemma is called function.surjective.exists instead of exists_congr_of_surjective.

#### Rob Lewis (Aug 06 2020 at 07:57):

Yury G. Kudryashov said:

That's why the lemma is called function.surjective.exists instead of exists_congr_of_surjective.

Yeah, proofs like that really show off all the work you put into renaming and refactoring!

Last updated: May 13 2021 at 19:20 UTC