iff_iff_not_or_and_or_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((\\\\neg a\\\\lor b)\\\\land(a\\\\lor\\\\neg b))$$$

Lean4

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

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