diagonal_subset_iff

Mathlib.Data.Set.Prod

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

English

A subset s of α×α contains the diagonal Δ(α) if and only if every pair (x,x) belongs to s.

Русский

Подмножество s ⊆ α×α содержит диагональ тогда, когда каждый элемент (x,x) принадлежит s.

LaTeX

$$$\\Delta(\\alpha) \\subseteq s \\iff \\forall x, (x,x) \\in s.$$$

Lean4

theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s := by rw [← range_diag, range_subset_iff]

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

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

Разделы

Аффилиация

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