product_cons

Mathlib.Data.List.ProdSigma

URI: https://scilib.ai/kg/mathlib#List.product_cons

English

For any a, l1, l2, the product (a :: l1) ×ˢ l2 equals map (λ b, (a,b)) l2 ++ (l1 ×ˢ l2).

Русский

Для любого a, l1, l2 выполняется (a :: l1) ×ˢ l2 = map (λ b, (a,b)) l2 ++ (l1 ×ˢ l2).

LaTeX

$$$ (a :: l_1) ×ˢ l_2 = map (\\lambda b, (a,b)) l_2 ++ (l_1 ×ˢ l_2)$$$

Lean4

@[simp]
theorem product_cons (a : α) (l₁ : List α) (l₂ : List β) : (a :: l₁) ×ˢ l₂ = map (fun b => (a, b)) l₂ ++ (l₁ ×ˢ l₂) :=
  rfl

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

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

Разделы

Аффилиация

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