prod — Mathlib

English

The Cartesian product Set.prod s t is the set of all pairs (a,b) with a ∈ s and b ∈ t.

Русский

Декартово произведение множества: все пары (a,b) такие, что a ∈ s и b ∈ t.

LaTeX

$$$$\\mathrm{prod}(s,t) = \\{(a,b)\\mid a\\in s \\\\land b\\in t\\}.$$$$

Lean4

/-- The Cartesian product `Set.prod s t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
def prod (s : Set α) (t : Set β) : Set (α × β) :=
  {p | p.1 ∈ s ∧ p.2 ∈ t}

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