### Nuprl Lemma : disjoint_increasing_onto

[m,n,k:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[g:ℕk ⟶ ℕm].
(m (n k) ∈ ℕsupposing
((∀j1:ℕn. ∀j2:ℕk.  ((f j1) (g j2) ∈ ℤ))) and
(∀i:ℕm. ((∃j:ℕn. (i (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i (g j) ∈ ℤ)))) and
increasing(g;k) and
increasing(f;n))

Proof

Definitions occuring in Statement :  increasing: increasing(f;k) int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] not: ¬A or: P ∨ Q apply: a function: x:A ⟶ B[x] add: m natural_number: \$n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: nat: so_lambda: λ2x.t[x] subtype_rel: A ⊆B int_seg: {i..j-} so_apply: x[s] all: x:A. B[x] implies:  Q guard: {T} sq_stable: SqStable(P) squash: T exists: x:A. B[x] or: P ∨ Q pi1: fst(t) lelt: i ≤ j < k and: P ∧ Q le: A ≤ B uiff: uiff(P;Q) subtract: m top: Top ge: i ≥  nat_plus: + less_than: a < b less_than': less_than'(a;b) true: True not: ¬A false: False decidable: Dec(P) inject: Inj(A;B;f) sq_type: SQType(T) bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality setElimination rename because_Cache sqequalRule lambdaEquality intEquality applyEquality functionExtensionality hypothesisEquality isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality dependent_set_memberEquality addEquality lambdaFormation independent_functionElimination imageMemberEquality baseClosed imageElimination dependent_functionElimination independent_isectElimination dependent_pairFormation unionEquality productEquality unionElimination productElimination independent_pairFormation sqequalIntensionalEquality promote_hyp voidElimination voidEquality minusEquality multiplyEquality addLevel levelHypothesis applyLambdaEquality instantiate cumulativity baseApply closedConclusion equalityElimination

Latex:
\mforall{}[m,n,k:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m].  \mforall{}[g:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}m].
(m  =  (n  +  k))  supposing
((\mforall{}j1:\mBbbN{}n.  \mforall{}j2:\mBbbN{}k.    (\mneg{}((f  j1)  =  (g  j2))))  and
(\mforall{}i:\mBbbN{}m.  ((\mexists{}j:\mBbbN{}n.  (i  =  (f  j)))  \mvee{}  (\mexists{}j:\mBbbN{}k.  (i  =  (g  j)))))  and
increasing(g;k)  and
increasing(f;n))

Date html generated: 2017_04_14-AM-07_34_06
Last ObjectModification: 2017_02_27-PM-03_12_59

Theory : fun_1

Home Index