mem_diag

Mathlib.Data.Finset.Prod

URI: https://scilib.ai/kg/mathlib#Finset.mem_diag

English

For any set S and any pair x=(a,b), x belongs to diag(S) exactly when a ∈ S and a=b.

Русский

Для множества S и пары x=(a,b) выполнено: x ∈ diag(S) тогда и только тогда, когда a ∈ S и a=b.

LaTeX

$$$(a,b) \\in \\mathrm{diag}(s) \\iff a \\in s \\land a = b$$$

Lean4

@[simp, grind =]
theorem mem_diag : x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2 := by simp +contextual [diag]

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

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

Разделы

Аффилиация

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