Mathlib.Data.List.TFAE

List.TFAE definition

(l : List Prop) : Prop

Full source

/-- TFAE: The Following (propositions) Are Equivalent.

The `tfae_have` and `tfae_finish` tactics can be useful in proofs with `TFAE` goals.
-/
def TFAE (l : List Prop) : Prop :=
  ∀ x ∈ l, ∀ y ∈ l, x ↔ y

The Following Are Equivalent (TFAE)

Informal description

For a list of propositions `l`, `TFAE l` means that all propositions in `l` are pairwise equivalent, i.e., for any two propositions `x` and `y` in `l`, `x` is equivalent to `y` (`x ↔ y`).

List.tfae_nil theorem

: TFAE []

Full source

theorem tfae_nil : TFAE [] :=
  forall_mem_nil _

TFAE Holds for Empty List

Informal description

The empty list of propositions satisfies the TFAE (The Following Are Equivalent) condition.

List.tfae_singleton theorem

(p) : TFAE [p]

Full source

@[simp]
theorem tfae_singleton (p) : TFAE [p] := by simp [TFAE, -eq_iff_iff]

TFAE Condition for Singleton List

Informal description

For any proposition $p$, the singleton list $[p]$ satisfies the "The Following Are Equivalent" (TFAE) condition, meaning all propositions in the list are pairwise equivalent. Since there's only one proposition in the list, this holds trivially.

List.tfae_cons_of_mem theorem

{a b} {l : List Prop} (h : b ∈ l) : TFAE (a :: l) ↔ (a ↔ b) ∧ TFAE l

Full source

theorem tfae_cons_of_mem {a b} {l : List Prop} (h : b ∈ l) : TFAETFAE (a :: l) ↔ (a ↔ b) ∧ TFAE l :=
  ⟨fun H => ⟨H a (by simp) b (Mem.tail a h),
    fun _ hp _ hq => H _ (Mem.tail a hp) _ (Mem.tail a hq)⟩,
      by
        rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
        · rfl
        · exact ab.trans (H _ h _ hq)
        · exact (ab.trans (H _ h _ hp)).symm
        · exact H _ hp _ hq⟩

Equivalence of TFAE for Cons with Membership Condition

Informal description

For any propositions $a$ and $b$ and a list of propositions $l$, if $b$ is an element of $l$, then the following are equivalent: 1. All propositions in the list $a :: l$ (i.e., $a$ prepended to $l$) are pairwise equivalent. 2. The proposition $a$ is equivalent to $b$ ($a \leftrightarrow b$) and all propositions in $l$ are pairwise equivalent.

List.tfae_cons_cons theorem

{a b} {l : List Prop} : TFAE (a :: b :: l) ↔ (a ↔ b) ∧ TFAE (b :: l)

Full source

theorem tfae_cons_cons {a b} {l : List Prop} : TFAETFAE (a :: b :: l) ↔ (a ↔ b) ∧ TFAE (b :: l) :=
  tfae_cons_of_mem (Mem.head _)

Equivalence of TFAE for Two-Element Prepended List

Informal description

For any propositions $a$ and $b$ and a list of propositions $l$, the following are equivalent: 1. All propositions in the list $a :: b :: l$ (i.e., $a$ and $b$ prepended to $l$) are pairwise equivalent. 2. The proposition $a$ is equivalent to $b$ ($a \leftrightarrow b$) and all propositions in the list $b :: l$ are pairwise equivalent.

List.tfae_cons_self theorem

{a} {l : List Prop} : TFAE (a :: a :: l) ↔ TFAE (a :: l)

Full source

@[simp]
theorem tfae_cons_self {a} {l : List Prop} : TFAETFAE (a :: a :: l) ↔ TFAE (a :: l) := by
  simp [tfae_cons_cons]

Equivalence of TFAE lists with duplicate head element

Informal description

For any proposition $a$ and list of propositions $l$, the statement that all propositions in the list $a :: a :: l$ are equivalent is equivalent to the statement that all propositions in the list $a :: l$ are equivalent. In other words, $TFAE(a :: a :: l) \leftrightarrow TFAE(a :: l)$.

List.tfae_of_forall theorem

(b : Prop) (l : List Prop) (h : ∀ a ∈ l, a ↔ b) : TFAE l

Full source

theorem tfae_of_forall (b : Prop) (l : List Prop) (h : ∀ a ∈ l, a ↔ b) : TFAE l :=
  fun _a₁ h₁ _a₂ h₂ => (h _ h₁).trans (h _ h₂).symm

Equivalence of Propositions in a List via Common Equivalence

Informal description

For any proposition $b$ and list of propositions $l$, if every proposition $a$ in $l$ is equivalent to $b$ (i.e., $a \leftrightarrow b$ for all $a \in l$), then all propositions in $l$ are pairwise equivalent (i.e., $\text{TFAE}(l)$ holds).

List.tfae_of_cycle theorem

{a b} {l : List Prop} (h_chain : List.Chain (· → ·) a (b :: l)) (h_last : getLastD l b → a) : TFAE (a :: b :: l)

Full source

theorem tfae_of_cycle {a b} {l : List Prop} (h_chain : List.Chain (· → ·) a (b :: l))
    (h_last : getLastD l b → a) : TFAE (a :: b :: l) := by
  induction l generalizing a b with
  | nil => simp_all [tfae_cons_cons, iff_def]
  | cons c l IH =>
    simp only [tfae_cons_cons, getLastD_cons, tfae_singleton, and_true, chain_cons, Chain.nil] at *
    rcases h_chain with ⟨ab, ⟨bc, ch⟩⟩
    have := IH ⟨bc, ch⟩ (ab ∘ h_last)
    exact ⟨⟨ab, h_last ∘ (this.2 c (.head _) _ getLastD_mem_cons).1 ∘ bc⟩, this⟩

Cycle of Implications Implies Equivalence of Propositions

Informal description

Given propositions $a$, $b$, and a list of propositions $l$, if there is a chain of implications from $a$ to $b$ through the elements of $l$ (i.e., $a \to b \to \cdots \to \text{last element of } l$) and the last implication $\text{last element of } l \to a$ holds, then all propositions in the list $a :: b :: l$ are pairwise equivalent (TFAE).

List.forall_tfae theorem

 {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) : (l.map (fun p ↦ ∀ a, p a)).TFAE

Full source

/-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∀ x, P₁ x) ↔ ... ↔ (∀ x, Pₙ x)`.
Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list
`[(∀ x, P₁ x), ..., (∀ x, Pₙ x)]`, but simply providing a list of underscores with the right
length makes it happier.

Example:
```lean
example (P₁ P₂ P₃ : ℕ → Prop) (H : ∀ n, [P₁ n, P₂ n, P₃ n].TFAE) :
    [∀ n, P₁ n, ∀ n, P₂ n, ∀ n, P₃ n].TFAE :=
  forall_tfae [_, _, _] H
```
-/
theorem forall_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) :
    (l.map (fun p ↦ ∀ a, p a)).TFAE := by
  simp only [TFAE, List.forall_mem_map]
  intros p₁ hp₁ p₂ hp₂
  exact forall_congr' fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Universal Quantification Preserves TFAE

Informal description

Let $\alpha$ be a type and $l$ be a list of predicates on $\alpha$. If for every $a \in \alpha$ the list $[P_1(a), \ldots, P_n(a)]$ satisfies TFAE (i.e., all $P_i(a)$ are pairwise equivalent), then the list of universal statements $[\forall a, P_1(a), \ldots, \forall a, P_n(a)]$ also satisfies TFAE (i.e., all $\forall a, P_i(a)$ are pairwise equivalent).

List.exists_tfae theorem

 {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) : (l.map (fun p ↦ ∃ a, p a)).TFAE

Full source

/-- If `P₁ x ↔ ... ↔ Pₙ x` for all `x`, then `(∃ x, P₁ x) ↔ ... ↔ (∃ x, Pₙ x)`.
Note: in concrete cases, Lean has trouble finding the list `[P₁, ..., Pₙ]` from the list
`[(∃ x, P₁ x), ..., (∃ x, Pₙ x)]`, but simply providing a list of underscores with the right
length makes it happier.

Example:
```lean
example (P₁ P₂ P₃ : ℕ → Prop) (H : ∀ n, [P₁ n, P₂ n, P₃ n].TFAE) :
    [∃ n, P₁ n, ∃ n, P₂ n, ∃ n, P₃ n].TFAE :=
  exists_tfae [_, _, _] H
```
-/
theorem exists_tfae {α : Type*} (l : List (α → Prop)) (H : ∀ a : α, (l.map (fun p ↦ p a)).TFAE) :
    (l.map (fun p ↦ ∃ a, p a)).TFAE := by
  simp only [TFAE, List.forall_mem_map]
  intros p₁ hp₁ p₂ hp₂
  exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

Equivalence of Existential Statements from Pointwise Equivalent Predicates

Informal description

Let $\alpha$ be a type and let $l = [P_1, \dots, P_n]$ be a list of predicates on $\alpha$. If for every $x \in \alpha$ the propositions $P_1(x), \dots, P_n(x)$ are pairwise equivalent (i.e., $P_i(x) \leftrightarrow P_j(x)$ for all $i,j$), then the existential statements $(\exists x, P_1(x)), \dots, (\exists x, P_n(x))$ are also pairwise equivalent.

List.tfae_not_iff theorem

{l : List Prop} : TFAE (l.map Not) ↔ TFAE l

Full source

theorem tfae_not_iff {l : List Prop} : TFAETFAE (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]

Equivalence of Negated Propositions in TFAE List

Informal description

For any list of propositions $l$, the statements in $l$ are pairwise equivalent if and only if their negations (i.e., the statements obtained by applying $\neg$ to each element of $l$) are pairwise equivalent. In other words, the following are equivalent: 1. For all $x, y \in l$, $x \leftrightarrow y$. 2. For all $x, y \in l$, $\neg x \leftrightarrow \neg y$.