Nuprl Definition : weak-overt
wOvert(X) == ∀[Y:Type]. ∃f:Open(X × Y) ⟶ Open(Y). ∀A:Open(X × Y). ∀y:Y. (y ∈ f A ⇐⇒ ¬¬(∃x:X. <x, y> ∈ A))
Definitions occuring in Statement :
in-open: x ∈ A,
Open: Open(X),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
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,
function: x:A ⟶ B[x],
Open: Open(X),
product: x:A × B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
not: ¬A,
exists: ∃x:A. B[x],
in-open: x ∈ A,
pair: <a, b>
FDL editor aliases :
weak-overt
Latex:
wOvert(X) ==
\mforall{}[Y:Type]. \mexists{}f:Open(X \mtimes{} Y) {}\mrightarrow{} Open(Y). \mforall{}A:Open(X \mtimes{} Y). \mforall{}y:Y. (y \mmember{} f A \mLeftarrow{}{}\mRightarrow{} \mneg{}\mneg{}(\mexists{}x:X. <x, y> \mmember{} A))
Date html generated:
2019_10_31-AM-07_19_11
Last ObjectModification:
2015_09_23-AM-09_29_01
Theory : synthetic!topology
Home
Index