Does this theorem exist in Mathlib?

Stream: new members

[Colin Jones ⚛️]

Does this theorem already exist in Mathlib4? If not could someone add it to a file? I have needed it for my work, but I have not found it in Mathlib.

import Mathlib

theorem not_and_and_and (P Q R : Prop) : ¬ (P ∧ Q ∧ R) ↔ (P → (¬ Q ∨ ¬ R)) := by
  rw [← not_and_or, ← not_and]

[Jireh Loreaux]

I would not expect Mathlib to have that fact as a single lemma. After all, you can get it just by pasting together two lemmas. That's what I would do in practice.

[Jireh Loreaux]

More generally, if you have arbitrary logical equivalences you need to transform between, if there is not a nice sequence of lemmas, you can just write down the two statements and prove they are equivalent by tauto.

[Colin Jones ⚛️]

Oh yeah, I forgot about tauto. That would make the logic a lot easier.

[Colin Jones ⚛️]

Thanks for reminding me.

[Notification Bot]

Colin Jones ⚛️ has marked this topic as resolved.

[Jireh Loreaux]

The only issue with tauto is that you would have to write out exactly what logical equivalence you wanted. So in your specific example, I think two rewrites is better.

[Notification Bot]

Colin Jones ⚛️ has marked this topic as unresolved.