Nuprl Definition : pair-lex
pair-lex(A;Ra;Rb) == λx,y. ((Ra (fst(x)) (fst(y))) ∨ (((fst(x)) = (fst(y)) ∈ A) ∧ (Rb (snd(x)) (snd(y)))))
Definitions occuring in Statement :
pi1: fst(t),
pi2: snd(t),
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T,
pi1: fst(t),
apply: f a,
pi2: snd(t)
FDL editor aliases :
pair-lex
Latex:
pair-lex(A;Ra;Rb) ==
\mlambda{}x,y. ((Ra (fst(x)) (fst(y))) \mvee{} (((fst(x)) = (fst(y))) \mwedge{} (Rb (snd(x)) (snd(y)))))
Date html generated:
2016_05_13-PM-03_18_31
Last ObjectModification:
2016_01_04-AM-10_27_06
Theory : well_fnd
Home
Index