Nuprl Lemma : null-bag-empty
∀T:Type. ∀x:bag(T). (↑bag-null(x) ⇐⇒ x = {} ∈ bag(T))
Proof
Definitions occuring in Statement :
assert: ↑b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
universe: Type,
equal: s = t ∈ T,
bag-null: bag-null(bs),
empty-bag: {},
bag: bag(T)
Lemmas :
equal-wf-T-base,
null-bag,
assert_wf,
null_wf3,
bag-subtype-list,
iff_wf,
bag_wf
Latex:
\mforall{}T:Type. \mforall{}x:bag(T). (\muparrow{}bag-null(x) \mLeftarrow{}{}\mRightarrow{} x = \{\})
Date html generated:
2015_07_23-AM-11_25_26
Last ObjectModification:
2015_01_28-PM-11_15_46
Home
Index