mem_product

Mathlib.Data.Multiset.Bind

URI: https://scilib.ai/kg/mathlib#Multiset.mem_product

English

An element p = (a,b) belongs to s ×ˢ t if and only if a ∈ s and b ∈ t a.

Русский

Элемент p = (a,b) принадлежит s ×ˢ t тогда и только тогда, когда a ∈ s и b ∈ t(a).

LaTeX

$$$p \in s \times^{\mathrm{SProd}} t \iff p.1 \in s \wedge p.2 \in t(p.1)$$$

Lean4

@[simp]
theorem mem_product : ∀ {p : α × β}, p ∈ @product α β s t ↔ p.1 ∈ s ∧ p.2 ∈ t
  | (a, b) => by simp [product, and_left_comm]

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

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

Разделы

Аффилиация

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