Nuprl Definition : up-set-lattice
up-set-lattice(T;eq;whole;x,y.le[x; y]) == sub-powerset-lattice(T;eq;whole;λs.∀x,y:T. (x ∈ s ⇒ le[x; y] ⇒ y ∈ s))
Definitions occuring in Statement :
sub-powerset-lattice: sub-powerset-lattice(T;eq;whole;P),
fset-member: a ∈ s,
all: ∀x:A. B[x],
implies: P ⇒ Q,
lambda: λx.A[x]
Definitions occuring in definition :
sub-powerset-lattice: sub-powerset-lattice(T;eq;whole;P),
lambda: λx.A[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
fset-member: a ∈ s
FDL editor aliases :
up-set-lattice
Latex:
up-set-lattice(T;eq;whole;x,y.le[x; y]) ==
sub-powerset-lattice(T;eq;whole;\mlambda{}s.\mforall{}x,y:T. (x \mmember{} s {}\mRightarrow{} le[x; y] {}\mRightarrow{} y \mmember{} s))
Date html generated:
2020_05_20-AM-08_47_40
Last ObjectModification:
2015_10_06-PM-01_44_01
Theory : lattices
Home
Index