image_prodMk_subset_prod_left

Mathlib.Data.Set.Prod

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

English

If b ∈ t, then { (a,b) : a ∈ s } ⊆ s × t.

Русский

Если b ∈ t, то множество { (a,b) : a ∈ s } ⊆ s × t.

LaTeX

$$$ (\{ (a,b) : a \in s \}) \subseteq s \times t \quad \text{каждому } b \in t $$$

Lean4

theorem image_prodMk_subset_prod_left (hb : b ∈ t) : (fun a => (a, b)) '' s ⊆ s ×ˢ t := by grind

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

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

Разделы

Аффилиация

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