Zulip Chat Archive

Stream: Is there code for X?

Topic: negation of funext?


view this post on Zulip Eric Rodriguez (Apr 07 2021 at 11:09):

Does example (f : α → β) (g : α → β) : f ≠ g ↔ ∃ a : α, f a ≠ g a exist? I've looked everywhere and I can't find it at all, but I refuse to believe this isn't in mathlib

view this post on Zulip Ruben Van de Velde (Apr 07 2021 at 11:38):

Apparently not? If you need a proof:

example {α β : Type*} (f : α  β) (g : α  β) : f  g   a : α, f a  g a :=
(not_congr function.funext_iff).trans not_forall

view this post on Zulip Eric Rodriguez (Apr 07 2021 at 11:41):

Proof was no big dealio was just confused it wasn't in mathlib ;b Feels like something worth PRing, I'd do it but you've written all the code now! Not sure where it'd fit in, maybe in logic.function.basic?

view this post on Zulip Eric Wieser (Apr 07 2021 at 11:49):

This doesn't scale very well - if we're going to add this lemma, we will probably want to add such a variant for every ext lemma in mathlib.

view this post on Zulip Kevin Buzzard (Apr 07 2021 at 11:57):

I guess if we have 1000 proofs of A    BA\iff B then I'm not sure we want 1000 new proofs of ¬A    ¬B\lnot A\iff \lnot B.

view this post on Zulip Eric Rodriguez (Apr 07 2021 at 11:57):

Would it maybe work better as an extension to the ext tactic, maybe ext!?

view this post on Zulip Eric Wieser (Apr 07 2021 at 14:01):

What's the goal state you ended up needing this for, @Eric Rodriguez?

view this post on Zulip Eric Rodriguez (Apr 07 2021 at 14:03):

Just looked, and I ended up deleting it, and just usingcontrapose! earlier. It probably makes the code far more readable, tbh


Last updated: May 19 2021 at 02:10 UTC