Documentation

Mathlib.Data.List.TFAE

The Following Are Equivalent #

This file allows to state that all propositions in a list are equivalent. It is used by Mathlib.Tactic.Tfae. TFAE l means ∀ x ∈ l, ∀ y ∈ l, x ↔ y. This is equivalent to Pairwise (↔) l.

def List.TFAE (l : List Prop) :

TFAE: The Following (propositions) Are Equivalent.

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

Equations
Instances For
    theorem List.tfae_nil :
    [].TFAE
    @[simp]
    theorem List.tfae_singleton (p : Prop) :
    [p].TFAE
    theorem List.tfae_cons_of_mem {a : Prop} {b : Prop} {l : List Prop} (h : b l) :
    (a :: l).TFAE (a b) l.TFAE
    theorem List.tfae_cons_cons {a : Prop} {b : Prop} {l : List Prop} :
    (a :: b :: l).TFAE (a b) (b :: l).TFAE
    @[simp]
    theorem List.tfae_cons_self {a : Prop} {l : List Prop} :
    (a :: a :: l).TFAE (a :: l).TFAE
    theorem List.tfae_of_forall (b : Prop) (l : List Prop) (h : ∀ (a : Prop), a l(a b)) :
    l.TFAE
    theorem List.tfae_of_cycle {a : Prop} {b : Prop} {l : List Prop} (h_chain : List.Chain (fun (x1 x2 : Prop) => x1x2) a (b :: l)) (h_last : l.getLastD ba) :
    (a :: b :: l).TFAE
    theorem List.TFAE.out {l : List Prop} (h : l.TFAE) (n₁ : Nat) (n₂ : Nat) {a : Prop} {b : Prop} (h₁ : autoParam (l.get? n₁ = some a) _auto✝) (h₂ : autoParam (l.get? n₂ = some b) _auto✝) :
    a b
    theorem List.forall_tfae {α : Type u_1} (l : List (αProp)) (H : ∀ (a : α), (List.map (fun (p : αProp) => p a) l).TFAE) :
    (List.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 : α), (List.map (fun (p : αProp) => p a) l).TFAE) :
    (List.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} :
    (List.map Not l).TFAE l.TFAE
    theorem List.TFAE.not {l : List Prop} :
    l.TFAE(List.map Not l).TFAE

    Alias of the reverse direction of List.tfae_not_iff.