entourageProd — Mathlib

English

Define entourageProd(u,v) to be the set of all pairs ((a1,b1),(a2,b2)) such that (a1,a2) ∈ u and (b1,b2) ∈ v.

Русский

Определим entourageProd(u,v) как множество всех пар ((a1,b1),(a2,b2)) таких, что (a1,a2) ∈ u и (b1,b2) ∈ v.

LaTeX

$$$\text{entourageProd}(u,v) := \{((a_1,b_1),(a_2,b_2))\mid (a_1,a_2)\in u \land (b_1,b_2)\in v\}$$$

Lean4

/-- An entourage of the diagonal in `α` and an entourage in `β` yield an entourage in `α × β`
once we permute coordinates. -/
def entourageProd (u : Set (α × α)) (v : Set (β × β)) : Set ((α × β) × α × β) :=
  {((a₁, b₁), (a₂, b₂)) | (a₁, a₂) ∈ u ∧ (b₁, b₂) ∈ v}

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