Nuprl Lemma : member_rset_neg_lemma
∀x,A:Top. (x ∈ -(A) ~ -(x) ∈ A)
Proof
Definitions occuring in Statement :
rset-neg: -(A),
rset-member: x ∈ A,
rminus: -(x),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
rset-neg: -(A),
rset-member: x ∈ A
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
hypothesis,
lemma_by_obid,
sqequalRule
Latex:
\mforall{}x,A:Top. (x \mmember{} -(A) \msim{} -(x) \mmember{} A)
Date html generated:
2016_05_18-AM-08_15_54
Last ObjectModification:
2015_12_28-AM-01_18_06
Theory : reals
Home
Index