Nuprl Lemma : fix_property

[T:Type]. ∀eq:EqDecider(T). ∀f:T ⟶ T.  (retraction(T;f)  (∀x:T. (((f f**(x)) f**(x) ∈ T) ∧ f**(x) is f*(x))))


Proof




Definitions occuring in Statement :  fix: f**(x) retraction: retraction(T;f) fun-connected: is f*(x) deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q retraction: retraction(T;f) exists: x:A. B[x] member: t ∈ T prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] and: P ∧ Q uimplies: supposing a so_apply: x[s] nat: le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A guard: {T} ge: i ≥  decidable: Dec(P) or: P ∨ Q uiff: uiff(P;Q) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top cand: c∧ B fix: f**(x) ycomb: Y eqof: eqof(d) deq: EqDecider(T) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff iff: ⇐⇒ Q rev_implies:  Q less_than: a < b squash: T
Lemmas referenced :  less_than_wf all_wf subtract_wf equal_wf fix_wf fun-connected_wf set_wf primrec-wf2 nat_wf add_nat_wf false_wf le_wf nat_properties decidable__le add-is-int-iff satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf itermAdd_wf intformeq_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_wf decidable__lt intformless_wf int_formula_prop_less_lemma retraction_wf deq_wf bool_wf equal-wf-T-base assert_wf bnot_wf not_wf eqof_wf uiff_transitivity eqtt_to_assert safe-assert-deq iff_transitivity iff_weakening_uiff eqff_to_assert assert_of_bnot fun-connected-test2 itermSubtract_wf int_term_value_subtract_lemma fun-connected_transitivity fun-connected-step decidable-equal-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut hypothesis addLevel sqequalHypSubstitution productElimination thin introduction extract_by_obid isectElimination applyEquality functionExtensionality hypothesisEquality cumulativity because_Cache sqequalRule natural_numberEquality rename setElimination lambdaEquality functionEquality productEquality independent_isectElimination intEquality equalityTransitivity equalitySymmetry dependent_functionElimination dependent_set_memberEquality addEquality independent_pairFormation applyLambdaEquality unionElimination pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll independent_functionElimination levelHypothesis universeEquality equalityElimination impliesFunctionality imageElimination

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}f:T  {}\mrightarrow{}  T.
        (retraction(T;f)  {}\mRightarrow{}  (\mforall{}x:T.  (((f  f**(x))  =  f**(x))  \mwedge{}  f**(x)  is  f*(x))))



Date html generated: 2018_05_21-PM-07_46_57
Last ObjectModification: 2017_07_26-PM-05_24_29

Theory : general


Home Index