diag_preimage_prod_self

Mathlib.Data.Set.Prod

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

English

The preimage of s × s under the diagonal map equals s.

Русский

Предобраз через диагональное отображение x ↦ (x, x) множества s × s равен s.

LaTeX

$$$(\\{ x\\in \\alpha : (x,x)\\in s\\times s\\}) = s$$$

Lean4

theorem diag_preimage_prod_self (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s :=
  inter_self s

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

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

Разделы

Аффилиация

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