Nuprl Definition : overt
Overt(X) ==
∀[Y:Type]. ∃ex:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀B:Open(Y). (∀y:Y. ex A y ≤ B y ⇐⇒ ∀x:X. ∀y:Y. A <x, y> ≤ B \000Cy)
Definitions occuring in Statement :
Open: Open(X),
sp-le: x ≤ y,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
pair: <a, b>,
product: x:A × B[x],
universe: Type
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
universe: Type,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
product: x:A × B[x],
Open: Open(X),
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
sp-le: x ≤ y,
pair: <a, b>,
apply: f a
FDL editor aliases :
overt
Latex:
Overt(X) ==
\mforall{}[Y:Type]
\mexists{}ex:Open(X \mtimes{} Y) {}\mrightarrow{} Open(Y)
\mforall{}A:Open(X \mtimes{} Y). \mforall{}B:Open(Y). (\mforall{}y:Y. ex A y \mleq{} B y \mLeftarrow{}{}\mRightarrow{} \mforall{}x:X. \mforall{}y:Y. A <x, y> \mleq{} B y)
Date html generated:
2019_10_31-AM-07_19_04
Last ObjectModification:
2015_09_23-AM-09_29_00
Theory : synthetic!topology
Home
Index