iff_iff_and_or_not_and_not — Mathlib

English

Let a and b be propositions. Then a ↔ b is equivalent to (a ∧ b) ∨ (¬a ∧ ¬b).

Русский

Пусть a и b — высказывания. Тогда a ⇔ b эквивалентно (a ∧ b) ∨ (¬a ∧ ¬b).

LaTeX

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

Lean4

theorem iff_iff_and_or_not_and_not : (a ↔ b) ↔ a ∧ b ∨ ¬a ∧ ¬b :=
  open scoped Classical in Decidable.iff_iff_and_or_not_and_not

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