preimage_fst_singleton_eq_range

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.preimage_fst_singleton_eq_range

English

For any b, the set of all pairs with second coordinate b is equal to α × {b}, i.e., snd^{-1}({b}) = α × {b}.

Русский

Для любого b множество пар с второй компонентой b равно α × {b}, т.е. snd^{-1}({b}) = α × {b}.

LaTeX

$$$\\mathrm{snd}^{-1}(\\{b\\}) = \\alpha \\times \\{b\\}$$$

Lean4

theorem preimage_fst_singleton_eq_range : (Prod.fst ⁻¹' { a } : Set (α × β)) = range (a, ·) := by grind

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

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

Разделы

Аффилиация

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