tfae_cons_of_mem — Mathlib

English

If b ∈ l, then TFAE (a :: l) is equivalent to (a ↔ b) ∧ TFAE l.

Русский

Если b ∈ l, то TFAE (a :: l) эквивалентно (a ↔ b) ∧ TFAE l.

LaTeX

$$$ \text{TFAE}(a :: l) \iff (a \leftrightarrow b) \land \text{TFAE}(l) $, при условии $b \in l$.$$

Lean4

theorem tfae_cons_of_mem {a b} {l : List Prop} (h : b ∈ l) : TFAE (a :: l) ↔ (a ↔ b) ∧ TFAE l :=
  ⟨fun H => ⟨H a (by simp) b (Mem.tail a h), fun _ hp _ hq => H _ (Mem.tail a hp) _ (Mem.tail a hq)⟩,
    by
    rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
    · rfl
    · exact ab.trans (H _ h _ hq)
    · exact (ab.trans (H _ h _ hp)).symm
    · exact H _ hp _ hq⟩

Похожие утверждения