chore(Data/List/TFAE): add tfae_not_iff (#10479)

leanprover-community · Feb 18, 2024 · efe0773 · efe0773
1 parent 2738601
commit efe0773
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/Mathlib/Data/List/TFAE.lean b/Mathlib/Data/List/TFAE.lean
@@ -114,4 +114,11 @@ theorem exists_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.ma
   exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem (fun p ↦ p a) hp₁)
     (p₂ a) (mem_map_of_mem (fun p ↦ p a) hp₂)
 
+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]
+
+alias ⟨_, TFAE.not⟩ := tfae_not_iff
+
 end List