Mathlib.Data.SProd

Module docstring

{"# Set Product Notation This file provides notation for a product of sets, and other similar types.

Main Definitions

SProd α β γ for a binary operation (· ×ˢ ·) : α → β → γ.

Notation

We introduce the notation x ×ˢ y for the sprod of any SProd structure. Ideally, x × y notation is desirable but this notation is defined in core for Prod so replacing x ×ˢ y with x × y seems difficult. "}

SProd structure

(α : Type u) (β : Type v) (γ : outParam (Type w))

Full source

/-- Notation type class for the set product `×ˢ`. -/
class SProd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  /-- The cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
  sprod : α → β → γ

Set product operation

Informal description

The structure `SProd α β γ` represents a binary operation `(· ×ˢ ·) : α → β → γ` that defines a product of sets (or similar types). This is used to introduce the notation `x ×ˢ y` for the product of elements `x` in `α` and `y` in `β`, resulting in an element of `γ`.

term_×ˢ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc SProd.sprod] infixr:82 " ×ˢ " => SProd.sprod

Set product notation

Informal description

The notation `×ˢ` represents a binary operation for set product (or similar product-like operations) between elements of types `α` and `β`, producing an element of type `γ`. This is denoted as `x ×ˢ y` for `x : α` and `y : β`.