@[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

• (⟨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.

@[simp]

theorem prod_eq {Ω : Type u_1} {S : Type u_2} {T : Type u_3} {X : Ω → S} {Y : Ω → T} {ω : Ω} : (⟨X, Y⟩) ω = (X ω, Y ω)