prod_insert — Mathlib

English

Inserting b into t within the second coordinate yields the union of the image of s under (·, b) with s × t.

Русский

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

LaTeX

$$$ s \times insert b t = (\mathrm{fun}\ a \Rightarrow (a,b)) '' s \cup (s \times t) $$$

Lean4

theorem prod_insert : s ×ˢ insert b t = (fun a => (a, b)) '' s ∪ s ×ˢ t := by
  simp only [insert_eq, prod_union, prod_singleton]

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