Nuprl Lemma : ocmon_subtype_omon

OCMon ⊆OMon


Proof




Definitions occuring in Statement :  ocmon: OCMon omon: OMon subtype_rel: A ⊆B
Definitions unfolded in proof :  ocmon: OCMon omon: OMon uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] prop: and: P ∧ Q abmonoid: AbMon mon: Mon so_lambda: λ2y.t[x; y] infix_ap: y so_apply: x[s1;s2] so_apply: x[s] uimplies: supposing a subtype_rel: A ⊆B all: x:A. B[x] implies:  Q cand: c∧ B
Lemmas referenced :  subtype_rel_sets abmonoid_wf ulinorder_wf grp_car_wf assert_wf grp_le_wf equal_wf bool_wf grp_eq_wf band_wf cancel_wf grp_op_wf uall_wf monot_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalTransitivity computationStep sqequalReflexivity cut instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis because_Cache lambdaEquality productEquality cumulativity setElimination rename hypothesisEquality applyEquality functionEquality independent_isectElimination setEquality lambdaFormation productElimination independent_pairFormation

Latex:
OCMon  \msubseteq{}r  OMon



Date html generated: 2018_05_21-PM-03_14_01
Last ObjectModification: 2018_05_19-AM-08_24_48

Theory : groups_1


Home Index