# 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.

source
class SProd (α : Type u) (β : Type v) (γ : outParam (Type w)) :
Type (max (max u v) w)

Notation type class for the set product `×ˢ`.

- sprod : α → β → γ

  The Cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.

Instances

source
def «term_×ˢ_» :
Lean.TrailingParserDescr

The Cartesian product `s ×ˢ t` is the set of `(a, b)` such that `a ∈ s` and `b ∈ t`.

Equations

- «term_×ˢ_» = Lean.ParserDescr.trailingNode `«term_×ˢ_» 82 83 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ˢ ") (Lean.ParserDescr.cat `term 82))

Instances For