range_sigmaMk — Mathlib

English

For fixed i, the range of the map Sigma.mk i is the set of all pairs with first component i.

Русский

Для фиксированного i множество образов Sigma.mk i равно множеству пар с первой компонентой i.

LaTeX

$$$\\mathrm{range}(\\Sigma\\!\\!\\mathrm{mk}\\n i) = \\Sigma\\mathrm{fst}^{-1} \\{i\\}$$$

Lean4

@[simp]
theorem range_sigmaMk (i : ι) : range (Sigma.mk i : α i → Sigma α) = Sigma.fst ⁻¹' { i } := by grind

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