Zulip Chat Archive

Stream: new members

Topic: iff with ∃ on both sides


view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 05 2020 at 21:38):

tauto can do the first implication.

view this post on Zulip Heather Macbeth (Aug 05 2020 at 21:39):

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

view this post on Zulip Patrick Massot (Aug 05 2020 at 21:41):

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

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 21:41):

There should be a lemma in data.equiv.basic

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 21:43):

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

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 21:44):

Let's try docs#function.surjective.exists

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 21:45):

(deleted)

view this post on Zulip Yury G. Kudryashov (Aug 05 2020 at 21:50):

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

view this post on Zulip 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!

view this post on Zulip Rob Lewis (Aug 05 2020 at 22:22):

Or even shorter, f.surjective.exists?

view this post on Zulip Heather Macbeth (Aug 05 2020 at 22:37):

Oops, yes!

view this post on Zulip Anatole Dedecker (Aug 05 2020 at 22:38):

Dot notation is awesome

view this post on Zulip 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.

view this post on Zulip 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