tfae_singleton

Mathlib.Data.List.TFAE

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

English

The TFAE of a singleton list is true, as simp shows.

Русский

Сложение TFAE единичного списка истинно; это следует из simp.

LaTeX

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

Lean4

@[simp]
theorem tfae_singleton (p) : TFAE [p] := by simp [TFAE, -eq_iff_iff]

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

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

Разделы

Аффилиация

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