The Following Are Equivalent

This file allows to state that all propositions in a list are equivalent. It is used by Mathlib/Tactic/Tfae.lean.

def List.TFAE (l : List Prop) : Prop

TFAE: The Following (propositions) Are Equivalent.

The tfae_have and tfae_finish tactics can be useful in proofs with TFAE goals.

Equations

• l.TFAE = ∀ (x : Prop), x ∈ l → ∀ (y : Prop), y ∈ l → (x ↔ y)

theorem List.tfae_nil : [].TFAE

@[simp]

theorem List.tfae_singleton (p : Prop) : [p].TFAE

theorem List.TFAE.subset {l₁ l₂ : List Prop} (h : l₂.TFAE) (hl : l₁ ⊆ l₂) : l₁.TFAE

theorem List.tfae_congr {l₁ l₂ : List Prop} (h₁₂ : l₁ ⊆ l₂) (h₂₁ : l₂ ⊆ l₁) : l₁.TFAE ↔ l₂.TFAE

theorem List.Perm.tfae_iff {l₁ l₂ : List Prop} (h : l₁.Perm l₂) : l₁.TFAE ↔ l₂.TFAE

@[simp]

theorem List.tfae_reverse {l : List Prop} : l.reverse.TFAE ↔ l.TFAE

theorem List.tfae_of_forall {b : Prop} {l : List Prop} (h : ∀ (a : Prop), a ∈ l → (a ↔ b)) : l.TFAE

theorem List.TFAE.out {l : List Prop} (h : l.TFAE) (i j : Nat) {a b : Prop} (h₁ : l[i - 1]? = some a := by rfl) (h₂ : l[j - 1]? = some b := by rfl) : autoParam (i ≠ 0) out._auto_5 → autoParam (j ≠ 0) out._auto_7 → (a ↔ b)

(TFAE [P₁, P₂, P₃, ...]).out i j, where i, j are the 1-indexed indices for TFAE statements, yields a proof of Pᵢ ↔ Pⱼ. Indices therefore must be greater than 0. This convention matches the statement numbering in tfae tactics.

theorem List.forall_tfae {α : Type u_1} (l : List (α → Prop)) (H : ∀ (a : α), (map (fun (p : α → Prop) => p a) l).TFAE) : (map (fun (p : α → Prop) => ∀ (a : α), p a) l).TFAE

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:

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 List.exists_tfae {α : Type u_1} (l : List (α → Prop)) (H : ∀ (a : α), (map (fun (p : α → Prop) => p a) l).TFAE) : (map (fun (p : α → Prop) => ∃ (a : α), p a) l).TFAE

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:

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 List.tfae_not_iff {l : List Prop} : (map Not l).TFAE ↔ l.TFAE

theorem List.TFAE.not {l : List Prop} : l.TFAE → (map Not l).TFAE

Alias of the reverse direction of List.tfae_not_iff.