not_and_or — Mathlib

English

One of De Morgan's laws: the negation of a conjunction is equivalent to the disjunction of the negations.

Русский

Одно из законов де Моргана: отрицание конъюнкции эквивалентно дизъюнкции отрицаний.

LaTeX

$$$\\\\neg(a\\\\land b)\\\\leftrightarrow(\\\\neg a\\\\lor\\\\neg b)$$$

Lean4

/-- One of **de Morgan's laws**: the negation of a conjunction is logically equivalent to the
disjunction of the negations. -/
theorem not_and_or : ¬(a ∧ b) ↔ ¬a ∨ ¬b :=
  open scoped Classical in Decidable.not_and_iff_not_or_not

Похожие утверждения