Nuprl Lemma : singleton-nat-missing-prop
∀x,y:ℕ. (↑member-nat-missing(x;singleton-nat-missing(y)) ⇐⇒ x = y ∈ ℕ)
Proof
Definitions occuring in Statement :
singleton-nat-missing: singleton-nat-missing(i),
member-nat-missing: member-nat-missing(i;s),
nat: ℕ,
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
equal: s = t ∈ T
Lemmas :
assert-member-nat-missing,
from-upto-member-nat,
false_wf,
le_wf,
less_than_wf,
not_over_and,
decidable__le,
decidable__equal_int,
not-equal-2,
add_functionality_wrt_le,
add-swap,
add-commutes,
le-add-cancel,
add-associates,
assert_wf,
member-nat-missing_wf,
singleton-nat-missing_wf,
sq_stable__le,
le_weakening,
less_than_transitivity1,
less_than_irreflexivity,
l_member_wf,
from-upto_wf,
subtype_rel_list,
subtype_rel_sets,
not_wf,
equal_wf,
nat_wf
\mforall{}x,y:\mBbbN{}. (\muparrow{}member-nat-missing(x;singleton-nat-missing(y)) \mLeftarrow{}{}\mRightarrow{} x = y)
Date html generated:
2015_07_17-AM-08_21_29
Last ObjectModification:
2015_04_02-PM-05_43_15
Home
Index