Nuprl Lemma : ss-ap_wf
∀[X,Y:SeparationSpace]. ∀[f:Point(X ⟶ Y)]. ∀[x:Point(X)]. (f(x) ∈ Point(Y))
Proof
Definitions occuring in Statement :
ss-ap: f(x),
ss-fun: X ⟶ Y,
ss-point: Point(ss),
separation-space: SeparationSpace,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
ss-ap: f(x),
top: Top,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
separation-space_wf,
ss-fun_wf,
ss-point_wf,
ss-fun-point
Rules used in proof :
because_Cache,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
hypothesisEquality,
applyEquality,
sqequalRule,
rename,
setElimination,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
isectElimination,
extract_by_obid,
sqequalHypSubstitution,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[X,Y:SeparationSpace]. \mforall{}[f:Point(X {}\mrightarrow{} Y)]. \mforall{}[x:Point(X)]. (f(x) \mmember{} Point(Y))
Date html generated:
2018_07_29-AM-10_11_46
Last ObjectModification:
2018_07_04-PM-00_03_03
Theory : constructive!algebra
Home
Index