### Nuprl Lemma : strict-fun-connected-step

`∀[T:Type]. ∀f:T ⟶ T. ∀x:T.  f x = f+(x) supposing ¬((f x) = x ∈ T)`

Proof

Definitions occuring in Statement :  strict-fun-connected: `y = f+(x)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` strict-fun-connected: `y = f+(x)` and: `P ∧ Q` cand: `A c∧ B` decidable: `Dec(P)` guard: `{T}` or: `P ∨ Q`
Lemmas referenced :  equal_wf fun-connected-step not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination extract_by_obid isectElimination cumulativity applyEquality functionExtensionality hypothesis rename independent_functionElimination equalitySymmetry independent_pairFormation because_Cache inrFormation functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x:T.    f  x  =  f+(x)  supposing  \mneg{}((f  x)  =  x)

Date html generated: 2018_05_21-PM-07_45_17
Last ObjectModification: 2017_07_26-PM-05_22_42

Theory : general

Home Index