Documentation

Mathlib.Data.SProd

Set Product Notation #

This file provides notation for a product of sets, and other similar types.

Main Definitions #

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)
  • sprod : αβγ

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

Notation type class for the set product ×ˢ.

Instances

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

    Equations
    Instances For