Theorem Marketplace

Theorem Details

-- De Morgan's law

theorem demorgan_not_or (P Q : Prop) : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) := by sorry

Bounty: 0.03 ETH

Status: Closed

Proof

open Classical

-- De Morgan's law

theorem demorgan_not_or (P Q : Prop) : ¬(P ∨ Q) ↔ (¬P ∧ ¬Q) :=
  Iff.intro
    (fun lhs : ¬(P ∨ Q) => show ¬P ∧ ¬Q from And.intro
      (fun hp : P => lhs (Or.intro_left Q hp))
      (fun hq : Q => lhs (Or.intro_right P hq)))
    (fun rhs : ¬P ∧ ¬Q => show ¬(P ∨ Q) from
      fun h : P ∨ Q =>
        Or.elim h rhs.left rhs.right)

Back to Bounties