Nuprl Lemma : cyclic-map-conjugate

[T:Type]. ∀[g,h:T ⟶ T].
  (∀[f:cyclic-map(T)]. (g (f h) ∈ cyclic-map(T))) supposing 
     ((∀a:T. ((g (h a)) a ∈ T)) and 
     (∀b:T. ((h (g b)) b ∈ T)))


Proof




Definitions occuring in Statement :  cyclic-map: cyclic-map(T) compose: g uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a cyclic-map: cyclic-map(T) injection: A →⟶ B so_lambda: λ2x.t[x] so_apply: x[s] exists: x:A. B[x] all: x:A. B[x] prop: inject: Inj(A;B;f) compose: g implies:  Q squash: T true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  all_wf exists_wf nat_wf equal_wf fun_exp_wf cyclic-map_wf compose_wf squash_wf true_wf iff_weakening_equal inject_wf iterated-conjugate2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename dependent_set_memberEquality extract_by_obid isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality hypothesis applyEquality functionExtensionality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache functionEquality universeEquality lambdaFormation applyLambdaEquality imageElimination dependent_functionElimination natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination dependent_pairFormation hyp_replacement

Latex:
\mforall{}[T:Type].  \mforall{}[g,h:T  {}\mrightarrow{}  T].
    (\mforall{}[f:cyclic-map(T)].  (g  o  (f  o  h)  \mmember{}  cyclic-map(T)))  supposing 
          ((\mforall{}a:T.  ((g  (h  a))  =  a))  and 
          (\mforall{}b:T.  ((h  (g  b))  =  b)))



Date html generated: 2018_05_21-PM-08_25_43
Last ObjectModification: 2017_07_26-PM-05_54_07

Theory : general


Home Index