Nuprl Lemma : null_mset_wf_f
∀s:DSet. (0{s} ∈ FiniteSet{s})
Proof
Definitions occuring in Statement :
finite_set: FiniteSet{s},
null_mset: 0{s},
all: ∀x:A. B[x],
member: t ∈ T,
dset: DSet
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
finite_set: FiniteSet{s},
le: A ≤ B,
and: P ∧ Q,
less_than': less_than'(a;b),
mset_count: x #∈ a,
count: a #∈ as,
mon_for: For{g} x ∈ as. f[x],
for: For{T,op,id} x ∈ as. f[x],
reduce: reduce(f;k;as),
list_ind: list_ind,
map: map(f;as),
null_mset: 0{s},
nil: [],
it: ⋅,
grp_id: e,
pi1: fst(t),
pi2: snd(t),
int_add_grp: <ℤ+>,
false: False,
not: ¬A,
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
dset: DSet,
subtype_rel: A ⊆r B,
nat: ℕ
Lemmas referenced :
null_mset_wf,
istype-false,
set_car_wf,
istype-le,
mset_count_wf,
dset_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
dependent_set_memberEquality_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
hypothesis,
sqequalRule,
independent_pairFormation,
natural_numberEquality,
universeIsType,
isectElimination,
setElimination,
rename,
functionIsType,
because_Cache,
applyEquality,
lambdaEquality_alt,
inhabitedIsType,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}s:DSet. (0\{s\} \mmember{} FiniteSet\{s\})
Date html generated:
2019_10_16-PM-01_06_51
Last ObjectModification:
2018_11_27-AM-10_31_00
Theory : mset
Home
Index