image_diag_union_image_offDiag

Mathlib.Data.Finset.Sym

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

← MathLib Explorer

English

The union of the diagonal and off-diagonal images equals s.sym2.

Русский

Объединение изображений диагонали и внедиагонали равно s.sym2.

LaTeX

$$s.diag.image \mathrm{Sym2.mk} \cup s.offDiag.image \mathrm{Sym2.mk} = s.sym2$$

Lean4

theorem image_diag_union_image_offDiag [DecidableEq α] : s.diag.image Sym2.mk ∪ s.offDiag.image Sym2.mk = s.sym2 := by
  rw [← image_union, diag_union_offDiag, sym2_eq_image]

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

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

Разделы

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

Аффилиация

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