Nuprl Lemma : comb_for_grp_leq_wf

λg,a,b,z. (a ≤ b) ∈ g:GrpSig ⟶ a:|g| ⟶ b:|g| ⟶ (↓True) ⟶ ℙ


Proof




Definitions occuring in Statement :  grp_leq: a ≤ b grp_car: |g| grp_sig: GrpSig prop: squash: T true: True member: t ∈ T lambda: λx.A[x] function: x:A ⟶ B[x]
Definitions unfolded in proof :  member: t ∈ T squash: T uall: [x:A]. B[x] prop:
Lemmas referenced :  grp_leq_wf squash_wf true_wf grp_car_wf grp_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid isectElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry

Latex:
\mlambda{}g,a,b,z.  (a  \mleq{}  b)  \mmember{}  g:GrpSig  {}\mrightarrow{}  a:|g|  {}\mrightarrow{}  b:|g|  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \mBbbP{}



Date html generated: 2016_05_15-PM-00_11_44
Last ObjectModification: 2015_12_26-PM-11_43_06

Theory : groups_1


Home Index