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 


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
Lemmas referenced :  all_wf int_seg_wf not_wf equal_wf or_wf exists_wf increasing_wf nat_wf injection_le add_nat_wf sq_stable__le le_wf lelt_wf set_subtype_base int_subtype_base add-member-int_seg1 add-associates minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul add-zero subtract_wf inject_wf add-commutes add_functionality_wrt_le le_reflexive zero-add one-mul two-mul mul-distributes-right less-iff-le not-lt-2 omega-shadow less_than_wf mul-distributes minus-add mul-associates mul-swap not-le-2 mul-commutes int_seg_properties nat_properties decidable__lt decidable__le subtype_base_sq le_weakening2 add-is-int-iff le-add-cancel le_transitivity lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot minus-zero increasing_inj equal-wf-T-base assert_wf le_int_wf bnot_wf uiff_transitivity assert_functionality_wrt_uiff bnot_of_lt_int assert_of_le_int le_antisymmetry
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

\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 

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

Theory : fun_1

Home Index