leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: new members

Topic: not and to not or


Marcus Rossel (Mar 10 2021 at 10:01):

Say I have ¬(a ∧ b ∧ c), how can I get ¬a ∨ ¬b ∨ ¬c from this?
So far I've found decidable.not_and_iff_or_not, but I'm hoping there's an easier way.

Marcus Rossel (Mar 10 2021 at 10:09):

Ok, found it :face_palm:‍♀️ not_and_distrib


Last updated: May 02 2025 at 03:31 UTC

Theme Simple by wildflame © 2016 Powered by jekyll