Nuprl Definition : power-set-lift

power-set-lift(T;R) == λA,B. ∀x:T. ((x ∈ A) ⇒ (∃y:T. ((y ∈ B) ∧ (R x y))))

Definitions occuring in Statement : set-member: (x ∈ s), all: ∀x:A. B[x], exists: ∃x:A. B[x], implies: P ⇒ Q, and: P ∧ Q, apply: f a, lambda: λx.A[x]
Definitions occuring in definition : lambda: λx.A[x], all: ∀x:A. B[x], implies: P ⇒ Q, exists: ∃x:A. B[x], and: P ∧ Q, set-member: (x ∈ s), apply: f a
FDL editor aliases : power-set-lift

Latex:
power-set-lift(T;R) == \mlambda{}A,B. \mforall{}x:T. ((x \mmember{} A) {}\mRightarrow{} (\mexists{}y:T. ((y \mmember{} B) \mwedge{} (R x y)))) Date html generated: 2016_05_13-PM-03_51_39 Last ObjectModification: 2015_09_22-PM-05_45_24 Theory : bar-induction Home Index