singleton_product — Mathlib

English

The product of a singleton {a} with t is the set of all pairs (a,b) with b ∈ t; i.e., {a} × t = { (a,b) | b ∈ t }.

Русский

Произведение единичного множества {a} и t состоит из всех пар (a,b) с b ∈ t; то есть {a} × t = { (a,b) | b ∈ t }.

LaTeX

$$$({a}) \\times t = \\{(a,b) \\mid b \\in t\\}$$$

Lean4

@[simp]
theorem singleton_product {a : α} : ({ a } : Finset α) ×ˢ t = t.map ⟨Prod.mk a, Prod.mk_right_injective _⟩ :=
  by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]

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