TFAE

Mathlib.Data.List.TFAE

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

← MathLib Explorer

English

The TFAE property holds for the empty list.

Русский

Свойство TFAE выполняется для пустого списка.

LaTeX

$$$ \text{TFAE}([]) $$$

Lean4

/-- TFAE: The Following (propositions) Are Equivalent.

The `tfae_have` and `tfae_finish` tactics can be useful in proofs with `TFAE` goals.
-/
def TFAE (l : List Prop) : Prop :=
  ∀ x ∈ l, ∀ y ∈ l, x ↔ y

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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