Nuprl Lemma : nat_subtype
ℕ ⊆r |(<ℤ+>↓hgrp)|
Proof
Definitions occuring in Statement :
int_add_grp: <ℤ+>,
hgrp_of_ocgrp: g↓hgrp,
grp_car: |g|,
nat: ℕ,
subtype_rel: A ⊆r B
Definitions unfolded in proof :
nat: ℕ,
grp_car: |g|,
pi1: fst(t),
hgrp_of_ocgrp: g↓hgrp,
hgrp_car: |g|+,
grp_leq: a ≤ b,
int_add_grp: <ℤ+>,
grp_le: ≤b,
pi2: snd(t),
grp_id: e,
infix_ap: x f y,
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
subtype_rel_sets,
le_wf,
assert_wf,
le_int_wf,
assert_of_le_int
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
intEquality,
because_Cache,
lambdaEquality,
natural_numberEquality,
hypothesisEquality,
hypothesis,
independent_isectElimination,
setElimination,
rename,
setEquality,
lambdaFormation,
productElimination
Latex:
\mBbbN{} \msubseteq{}r |(<\mBbbZ{}+>\mdownarrow{}hgrp)|
Date html generated:
2018_05_21-PM-03_14_17
Last ObjectModification:
2018_05_19-AM-08_26_15
Theory : groups_1
Home
Index