tfae_nil

Mathlib.Data.List.TFAE

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

English

For any proposition p, the list [p] has the TFAE property.

Русский

Для любой пропозиции p список [p] удовлетворяет свойству TFAE.

LaTeX

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

Lean4

theorem tfae_nil : TFAE [] :=
  forall_mem_nil _

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

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

Разделы

Аффилиация

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