tfae_not_iff — Mathlib

English

The TFAE relation is invariant under negation: TFAE (l.map Not) is equivalent to TFAE l.

Русский

Отрицание сохраняет отношения TFAE: TFAE (l.map Not) эквивалентно TFAE l.

LaTeX

$$$ \text{TFAE}(l.map Not) \leftrightarrow \text{TFAE}(l) $$$

Lean4

theorem tfae_not_iff {l : List Prop} : TFAE (l.map Not) ↔ TFAE l := by
  classical simp only [TFAE, mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Decidable.not_iff_not]

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