Nuprl Definition : strong-overt
sOvert(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),
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 :
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,
exists: ∃x:A. B[x],
in-open: x ∈ A,
pair: <a, b>
FDL editor aliases :
strong-overt
Latex:
sOvert(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{} \mexists{}x:X. <x, y> \mmember{}\000C A)
Date html generated:
2019_10_31-AM-07_19_22
Last ObjectModification:
2015_09_23-AM-09_29_02
Theory : synthetic!topology
Home
Index