diag_inter

Mathlib.Data.Finset.Prod

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

English

The diagonal of the intersection equals the intersection of diagonals: (S ∩ T).diag = S.diag ∩ T.diag.

Русский

Диагональ пересечения равна пересечению диагоналей: (S ∩ T).diag = S.diag ∩ T.diag.

LaTeX

$$$(s \\cap t).\\mathrm{diag} = s.\\mathrm{diag} \\cap t.\\mathrm{diag}$$$

Lean4

theorem diag_inter : (s ∩ t).diag = s.diag ∩ t.diag := by grind

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

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

Разделы

Аффилиация

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