mathlib3 documentation

data.list.tfae

The Following Are Equivalent #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file allows to state that all propositions in a list are equivalent. It is used by tactic.tfae. tfae l means ∀ x ∈ l, ∀ y ∈ l, x ↔ y. This is equivalent to pairwise (↔) l.

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
theorem list.tfae_singleton (p : Prop) :
theorem list.tfae_cons_of_mem {a b : Prop} {l : list Prop} (h : b l) :
(a :: l).tfae (a b) l.tfae
theorem list.tfae_cons_cons {a b : Prop} {l : list Prop} :
(a :: b :: l).tfae (a b) (b :: l).tfae
theorem list.tfae_of_forall (b : Prop) (l : list Prop) (h : (a : Prop), a l (a b)) :
theorem list.tfae_of_cycle {a b : Prop} {l : list Prop} :
list.chain (λ (_x _y : Prop), _x _y) a (b :: l) (list.ilast' b l a) (a :: b :: l).tfae
theorem list.tfae.out {l : list Prop} (h : l.tfae) (n₁ n₂ : ) {a b : Prop} (h₁ : l.nth n₁ = option.some a . "refl") (h₂ : l.nth n₂ = option.some b . "refl") :
a b