Zulip Chat Archive

Stream: Is there code for X?

Topic: negation of funext?


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

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

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?

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.

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.

Eric Rodriguez (Apr 07 2021 at 11:57):

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

Eric Wieser (Apr 07 2021 at 14:01):

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

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: Dec 20 2023 at 11:08 UTC