Nuprl Lemma : ocgrp_subtype_abgrp

OGrp ⊆AbGrp


Proof




Definitions occuring in Statement :  ocgrp: OGrp abgrp: AbGrp subtype_rel: A ⊆B
Definitions unfolded in proof :  subtype_rel: A ⊆B member: t ∈ T ocgrp: OGrp ocmon: OCMon abmonoid: AbMon abgrp: AbGrp grp: Group{i} uall: [x:A]. B[x] mon: Mon prop: and: P ∧ Q so_lambda: λ2y.t[x; y] infix_ap: y so_apply: x[s1;s2] all: x:A. B[x] or: P ∨ Q uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} uiff: uiff(P;Q) bfalse: ff band: p ∧b q ifthenelse: if then else fi  so_lambda: λ2x.t[x] so_apply: x[s] sq_stable: SqStable(P) squash: T
Lemmas referenced :  subtype_rel_sets mon_wf comm_wf grp_car_wf grp_op_wf ulinorder_wf assert_wf grp_le_wf equal_wf bool_wf grp_eq_wf bool_cases subtype_base_sq bool_subtype_base eqtt_to_assert band_wf btrue_wf bfalse_wf cancel_wf monot_wf inverse_wf grp_id_wf grp_inv_wf sq_stable__comm ocgrp_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality_alt cut hypothesisEquality applyEquality thin sqequalRule instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination setEquality hypothesis cumulativity setElimination rename because_Cache productEquality inhabitedIsType universeIsType functionEquality dependent_functionElimination unionElimination independent_isectElimination equalityTransitivity equalitySymmetry independent_functionElimination productElimination isectEquality setIsType productIsType equalityIstype functionIsType isectIsType lambdaFormation_alt imageMemberEquality baseClosed imageElimination

Latex:
OGrp  \msubseteq{}r  AbGrp



Date html generated: 2020_05_19-PM-10_07_51
Last ObjectModification: 2020_01_08-PM-05_59_42

Theory : groups_1


Home Index