Nuprl Lemma : mon_when_wf

[g:IMonoid]. ∀[b:𝔹]. ∀[p:|g|].  (when b. p ∈ |g|)


Proof




Definitions occuring in Statement :  mon_when: when b. p imon: IMonoid grp_car: |g| bool: 𝔹 uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  mon_when: when b. p uall: [x:A]. B[x] member: t ∈ T imon: IMonoid
Lemmas referenced :  ifthenelse_wf grp_car_wf grp_id_wf bool_wf imon_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality setElimination rename hypothesis axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[g:IMonoid].  \mforall{}[b:\mBbbB{}].  \mforall{}[p:|g|].    (when  b.  p  \mmember{}  |g|)



Date html generated: 2016_05_15-PM-00_18_27
Last ObjectModification: 2015_12_26-PM-11_38_25

Theory : groups_1


Home Index