Nuprl Lemma : item_mk_set_lemma
∀x,f,T:Top. (set-item(f"(T);x) ~ f x)
Proof
Definitions occuring in Statement :
mk-set: f"(T),
set-item: set-item(s;x),
top: Top,
all: ∀x:A. B[x],
apply: f a,
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
pi2: snd(t),
Wsup: Wsup(a;b),
set-item: set-item(s;x),
mk-set: f"(T)
Lemmas referenced :
top_wf
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut,
lambdaFormation,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution
Latex:
\mforall{}x,f,T:Top. (set-item(f"(T);x) \msim{} f x)
Date html generated:
2018_07_29-AM-09_50_33
Last ObjectModification:
2018_07_11-PM-03_12_00
Theory : constructive!set!theory
Home
Index