mk_preimage_prod_left

Mathlib.Data.Set.Prod

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

English

If b ∈ t, then (a ↦ (a,b))^{-1}(s × t) = s.

Русский

Пусть b ∈ t. Тогда (a ↦ (a,b))^{-1}(s × t) = s.

LaTeX

$$$ (\lambda a:(\alpha), (a,b))^{-1}'(s \times t) = s \quad \text{if } b \in t $$$

Lean4

@[simp]
theorem mk_preimage_prod_left (hb : b ∈ t) : (fun a => (a, b)) ⁻¹' s ×ˢ t = s := by grind

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

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

Разделы

Аффилиация

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