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
.
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)