1 parent 465c566 commit 5f10dabCopy full SHA for 5f10dab
1 file changed
Mathlib/Data/List/Pairwise.lean
@@ -160,7 +160,7 @@ theorem tfae_iff_pairwise : TFAE l ↔ l.Pairwise (· ↔ ·) :=
160
⟨pairwise_of_forall_mem_list, Pairwise.forall_of_forall fun _ _ ↦ .rfl⟩
161
162
theorem tfae_append :
163
- TFAE (l₁ ++ l₂) ↔ TFAE l₁ ∧ TFAE l₂ ∧ (∀ a ∈ l₁, ∀ b ∈ l₂, (a ↔ b)) := by
+ TFAE (l₁ ++ l₂) ↔ TFAE l₁ ∧ TFAE l₂ ∧ (∀ a ∈ l₁, ∀ b ∈ l₂, a ↔ b) := by
164
simp [tfae_iff_pairwise, pairwise_append]
165
166
theorem tfae_append_of_mem (ha : a ∈ l₁) (hb : b ∈ l₂) :
0 commit comments