insert_prod — Mathlib

English

Inserting an element a into s corresponds to the union of the image of t under (a,·) with s × t.

Русский

Вставка элемента a в s соответствует объединению образа t под отображением (a,·) с s × t.

LaTeX

$$$ \mathrm{insert}\ a\ s \times t = (\mathrm{Prod.mk} \, a) '' t \cup (s \times t) $$$

Lean4

theorem insert_prod : insert a s ×ˢ t = Prod.mk a '' t ∪ s ×ˢ t := by simp only [insert_eq, union_prod, singleton_prod]

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