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∀ x ∈ l, ∀ y ∈ l, x ↔ y∈ l, ∀ y ∈ l, x ↔ y∀ y ∈ l, x ↔ y∈ l, x ↔ y↔ y. This is equivalent to pairwise (↔) l↔) l.

ink

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

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

ink

theorem List.tfae_nil : List.TFAE []

ink

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

ink

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

ink

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

ink

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

ink

theorem List.tfae_of_cycle {a : Prop} {b : Prop} {l : List Prop} : List.Chain (fun x x_1 => x → x_1) a (b :: l) → (List.ilast' b l → a) → List.TFAE (a :: b :: l)

ink

theorem List.TFAE.out {l : List Prop} (h : List.TFAE l) (n₁ : ℕ) (n₂ : ℕ) {a : Prop} {b : Prop} (h₁ : autoParam (List.get? l n₁ = some a) _auto✝) (h₂ : autoParam (List.get? l n₂ = some b) _auto✝) : a ↔ b