tfae_cons_cons

Mathlib.Data.List.TFAE

URI: https://scilib.ai/kg/mathlib#List.tfae_cons_cons

English

TFAE (a :: b :: l) is equivalent to (a ↔ b) ∧ TFAE (b :: l).

Русский

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

LaTeX

$$$ \text{TFAE}(a :: b :: l) \iff (a \leftrightarrow b) \land \text{TFAE}(b :: l) $$$

Lean4

theorem tfae_cons_cons {a b} {l : List Prop} : TFAE (a :: b :: l) ↔ (a ↔ b) ∧ TFAE (b :: l) :=
  tfae_cons_of_mem (Mem.head _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru