mk_preimage_prod_right_eq_empty

Mathlib.Data.Set.Prod

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

English

If a ∉ s, then Prod.mk a ⁻¹'(s × t) = ∅.

Русский

Если a ∉ s, то Prod.mk a ⁻¹'(s × t) = ∅.

LaTeX

$$$ (Prod.mk a)^{-1}'(s \times t) = \emptyset \quad \text{if } a \notin s $$$

Lean4

@[simp]
theorem mk_preimage_prod_right_eq_empty (ha : a ∉ s) : Prod.mk a ⁻¹' s ×ˢ t = ∅ := by grind

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

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

Разделы

Аффилиация

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