diagonal_nonempty

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.diagonal_nonempty

English

The diagonal Δ(α) is nonempty whenever α is nonempty.

Русский

Диагональ Δ(α) непустая тогда, когда α непусто.

LaTeX

$$$(\\Delta(\\alpha)) \\neq \\emptyset,$ если $α$ пусто?$$$

Lean4

theorem diagonal_nonempty [Nonempty α] : (diagonal α).Nonempty :=
  Nonempty.elim ‹_› fun x => ⟨_, mem_diagonal x⟩

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

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

Разделы

Аффилиация

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