preimage_snd_singleton_eq_range — Mathlib

English

The preimage under the second projection of a singleton {b} equals the range of the map a ↦ (a,b).

Русский

Предобраз подмножества {b} по второй проекции равен образу функции a ↦ (a,b).

LaTeX

$$$$ (\\mathrm{Prod}.{\\mathrm snd})^{-1}\\{ b \\} = \\operatorname{range}(\\lambda a.\, (a,b)) $$$$

Lean4

theorem preimage_snd_singleton_eq_range : (Prod.snd ⁻¹' { b } : Set (α × β)) = range (·, b) := by grind

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