prod_eq

Mathlib.Data.Set.Operations

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

English

The product s ×ˢ t equals fst^{-1}(s) ∩ snd^{-1}(t).

Русский

Произведение s ×ˢ t равно fst^{-1}(s) ∩ snd^{-1}(t).

LaTeX

$$$$s \\times\\!\\!ˢ t = \\mathrm{fst}^{-1}'(s) \\cap \\mathrm{snd}^{-1}'(t).$$$$

Lean4

theorem prod_eq (s : Set α) (t : Set β) : s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t :=
  rfl

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

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

Разделы

Аффилиация

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