mathlib documentation

data.list.tfae

def list.tfae  :
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
  • l.tfae = ∀ (x : Prop), x l∀ (y : Prop), y l(x y)
theorem list.tfae_singleton (p : Prop) :
[p].tfae

theorem list.tfae_cons_of_mem {a b : Prop} {l : list Prop} :
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) :
(∀ (a : Prop), a l(a b)) → l.tfae

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} :
(l.nth n₁ = some a . "refl")(l.nth n₂ = some b . "refl")(a b)