diagonal_eq_univ_iff

Mathlib.Data.Set.Prod

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

← MathLib Explorer

English

The diagonal equals the universal set if and only if α is a subsingleton.

Русский

Диагональ равна множествоuniv тогда и только тогда, когда α — пододинство.

LaTeX

$$$\\Delta(\\alpha) = \\mathrm{univ} \\iff \\text{Subsingleton}(\\alpha)$$$

Lean4

theorem diagonal_eq_univ_iff : diagonal α = univ ↔ Subsingleton α := by
  simp only [subsingleton_iff, eq_univ_iff_forall, Prod.forall, mem_diagonal_iff]

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

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

Разделы

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

Аффилиация

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