Nuprl Lemma : nat_inc

ℕ ⊆|(<ℤ+>↓hgrp)|


Proof




Definitions occuring in Statement :  int_add_grp: <ℤ+> hgrp_of_ocgrp: g↓hgrp grp_car: |g| nat: subtype_rel: A ⊆B
Definitions unfolded in proof :  nat: grp_car: |g| pi1: fst(t) hgrp_of_ocgrp: g↓hgrp hgrp_car: |g|+ int_add_grp: <ℤ+> grp_id: e pi2: snd(t) grp_leq: a ≤ b grp_le: b infix_ap: y uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a subtype_rel: A ⊆B prop: all: x:A. B[x] implies:  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: 2019_10_15-AM-10_33_08
Last ObjectModification: 2018_09_17-PM-06_22_05

Theory : groups_1


Home Index