Nuprl Definition : convergent-flow

convergent-flow(es;X;f) ==
(∀x,y:E(X). ((¬((f x) = x ∈ E(X))) ⇒ (¬((f y) = y ∈ E(X))) ⇒ (loc(f x) = loc(f y) ∈ Id) ⇒ (loc(x) = loc(y) ∈ Id)))
∧ (∀x,y:E(X). (x is f*(y) ⇒ (¬(x = y ∈ E)) ⇒ (¬(loc(x) = loc(y) ∈ Id))))

Definitions occuring in Statement : es-E-interface: E(X), es-loc: loc(e), es-E: E, Id: Id, all: ∀x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, apply: f a, equal: s = t ∈ T, fun-connected: y is f*(x)
FDL editor aliases : convergent-flow
convergent-flow(es;X;f) == (\mforall{}x,y:E(X). ((\mneg{}((f x) = x)) {}\mRightarrow{} (\mneg{}((f y) = y)) {}\mRightarrow{} (loc(f x) = loc(f y)) {}\mRightarrow{} (loc(x) = loc(y)))) \mwedge{} (\mforall{}x,y:E(X). (x is f*(y) {}\mRightarrow{} (\mneg{}(x = y)) {}\mRightarrow{} (\mneg{}(loc(x) = loc(y))))) Date html generated: 2015_07_17-PM-00_58_50 Last ObjectModification: 2012_02_25-PM-01_31_27 Home Index