Nuprl Definition : grp_sig
GrpSig == car:Type × eq:car ⟶ car ⟶ 𝔹 × le:car ⟶ car ⟶ 𝔹 × op:car ⟶ car ⟶ car × id:car × (car ⟶ car)
Definitions occuring in Statement :
bool: 𝔹,
function: x:A ⟶ B[x],
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
universe: Type,
bool: 𝔹,
product: x:A × B[x],
function: x:A ⟶ B[x]
Latex:
GrpSig ==
car:Type \mtimes{} eq:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{} \mtimes{} le:car {}\mrightarrow{} car {}\mrightarrow{} \mBbbB{} \mtimes{} op:car {}\mrightarrow{} car {}\mrightarrow{} car \mtimes{} id:car \mtimes{} (car {}\mrightarrow{} car)
Date html generated:
2016_05_15-PM-00_06_11
Last ObjectModification:
2015_09_23-AM-06_24_12
Theory : groups_1
Home
Index