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.

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.