mathlib docs: data.list.tfae

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_nil :

theorem list.tfae_singleton (p : Prop) :

theorem list.tfae_cons_of_mem {a b : Prop} {l : list Prop} (h : b ∈ l) :

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} (a_1 : list.chain (λ (_x _y : Prop), _x → _y) a (b :: l)) (a_2 : 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₁ = some a . "refl") (h₂ : l.nth n₂ = some b . "refl") :

a ↔ b