@[reducible, inline]

abbrev prod {Ω : Type u_1} {S : Type u_2} {T : Type u_3} (X : Ω → S) (Y : Ω → T) (ω : Ω) : S × T

The pair of two random variables

Equations

• prod X Y ω = (X ω, Y ω)

def «term⟨_,_⟩» : Lean.ParserDescr

The pair of two random variables

Equations

• One or more equations did not get rendered due to their size.

def «term⟨_,_⟩».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.