mem_entourageProd — Mathlib

English

Membership in entourageProd u v is equivalent to (a1,a2) ∈ u and (b1,b2) ∈ v for the corresponding components.

Русский

Членство в entourageProd u v эквивалентно тому, что соответствующие пары принадлежат u и v по компонентам.

LaTeX

$$$p \in entou rageProd(u,v) \Leftrightarrow (p.1.1,p.2.1) \in u \land (p.1.2,p.2.2) \in v$$$

Lean4

theorem mem_entourageProd {u : Set (α × α)} {v : Set (β × β)} {p : (α × β) × α × β} :
    p ∈ entourageProd u v ↔ (p.1.1, p.2.1) ∈ u ∧ (p.1.2, p.2.2) ∈ v :=
  Iff.rfl

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