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]