mem_product — Mathlib

English

An ordered pair (a,b) belongs to l1 ×ˢ l2 iff a ∈ l1 and b ∈ l2.

Русский

Парa (a,b) принадлежит l1 ×ˢ l2 тогда и только тогда, когда a ∈ l1 и b ∈ l2.

LaTeX

$$$(a,b) \in l_1 ×ˢ l_2 \iff a \in l_1 \land b \in l_2$$$

Lean4

@[simp]
theorem mem_product {l₁ : List α} {l₂ : List β} {a : α} {b : β} : (a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ := by
  simp_all [SProd.sprod, product, mem_flatMap, mem_map, Prod.ext_iff, and_left_comm, exists_and_left, exists_eq_left,
    exists_eq_right]

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