### Nuprl Lemma : bijection_restriction

`∀k:ℕ. ∀f:ℕk ⟶ ℕk.`
`  Bij(ℕk;ℕk;f) `` {(f ∈ ℕk - 1 ⟶ ℕk - 1) ∧ Bij(ℕk - 1;ℕk - 1;f)} supposing (f (k - 1)) = (k - 1) ∈ ℤ supposing 0 < k`

Proof

Definitions occuring in Statement :  biject: `Bij(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` guard: `{T}` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` apply: `f a` function: `x:A ⟶ B[x]` subtract: `n - m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` implies: `P `` Q` guard: `{T}` and: `P ∧ Q` cand: `A c∧ B` prop: `ℙ` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` subtract: `n - m` subtype_rel: `A ⊆r B` top: `Top` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` less_than: `a < b` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` biject: `Bij(A;B;f)` inject: `Inj(A;B;f)` squash: `↓T` surject: `Surj(A;B;f)`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename hypothesisEquality hypothesis independent_isectElimination axiomEquality equalityTransitivity equalitySymmetry independent_pairFormation intEquality applyEquality functionExtensionality because_Cache dependent_set_memberEquality dependent_functionElimination unionElimination voidElimination productElimination independent_functionElimination addEquality sqequalRule lambdaEquality isect_memberEquality voidEquality minusEquality functionEquality dependent_pairFormation sqequalIntensionalEquality promote_hyp multiplyEquality instantiate cumulativity applyLambdaEquality imageMemberEquality baseClosed

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}k.
Bij(\mBbbN{}k;\mBbbN{}k;f)  {}\mRightarrow{}  \{(f  \mmember{}  \mBbbN{}k  -  1  {}\mrightarrow{}  \mBbbN{}k  -  1)  \mwedge{}  Bij(\mBbbN{}k  -  1;\mBbbN{}k  -  1;f)\}  supposing  (f  (k  -  1))  =  (k  -  1)
supposing  0  <  k

Date html generated: 2017_04_14-AM-07_34_14
Last ObjectModification: 2017_02_27-PM-03_08_51

Theory : fun_1

Home Index