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.

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))