Nuprl Lemma : ss-map_wf

[X,Y:SeparationSpace]. ∀[f:Point(X) ⟶ Point(Y)].  (ss-map(X;Y;f) ∈ ℙ)


Proof




Definitions occuring in Statement :  ss-map: ss-map(X;Y;f) ss-point: Point(ss) separation-space: SeparationSpace uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  so_apply: x[s] prop: implies:  Q so_lambda: λ2x.t[x] ss-map: ss-map(X;Y;f) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  separation-space_wf ss-sep_wf ss-point_wf all_wf
Rules used in proof :  because_Cache isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality applyEquality functionEquality lambdaEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[X,Y:SeparationSpace].  \mforall{}[f:Point(X)  {}\mrightarrow{}  Point(Y)].    (ss-map(X;Y;f)  \mmember{}  \mBbbP{})



Date html generated: 2018_07_29-AM-10_10_42
Last ObjectModification: 2018_06_28-PM-03_03_51

Theory : constructive!algebra


Home Index