singleton_sigma — Mathlib

English

The sigma over a singleton index set equals all pairs with that index and corresponding elements.

Русский

Сигма над единичным множеством индексов равна всем парам с этой индексной частью и соответствующими элементами.

LaTeX

$$$(\\{i\\} : Set ι).\\sigma t = \\{(i,a) : a\\in t(i)\\}$$$

Lean4

@[simp]
theorem singleton_sigma : ({ i } : Set ι).sigma t = Sigma.mk i '' t i := by grind

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