Nuprl Lemma : dom_mk_set_lemma
∀f,T:Top. (set-dom(f"(T)) ~ T)
Proof
Definitions occuring in Statement :
mk-set: f"(T),
set-dom: set-dom(s),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
pi1: fst(t),
Wsup: Wsup(a;b),
set-dom: set-dom(s),
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{}f,T:Top. (set-dom(f"(T)) \msim{} T)
Date html generated:
2018_07_29-AM-09_50_31
Last ObjectModification:
2018_07_11-PM-03_10_40
Theory : constructive!set!theory
Home
Index