### Nuprl Lemma : funinv_wf

`∀[n,m:ℕ]. ∀[f:{f:ℕn ⟶ ℕm| Surj(ℕn;ℕm;f)} ].  (inv(f) ∈ {g:ℕm ⟶ ℕn| Inj(ℕm;ℕn;g) ∧ (∀x:ℕm. ((f (g x)) = x ∈ ℤ))} )`

Proof

Definitions occuring in Statement :  funinv: `inv(f)` surject: `Surj(A;B;f)` inject: `Inj(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  funinv: `inv(f)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` prop: `ℙ` top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` or: `P ∨ Q` decidable: `Dec(P)` and: `P ∧ Q` lelt: `i ≤ j < k` ge: `i ≥ j ` guard: `{T}` exists: `∃x:A. B[x]` uimplies: `b supposing a` nat: `ℕ` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` surject: `Surj(A;B;f)` member: `t ∈ T` uall: `∀[x:A]. B[x]` cand: `A c∧ B` inject: `Inj(A;B;f)`
Lemmas referenced :  nat_wf surject_wf set_wf exists_wf assert_wf assert_of_eq_int equal_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int nat_properties int_seg_properties int_seg_wf eq_int_wf mu-bound-property+ inject_wf all_wf decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf and_wf
Rules used in proof :  functionEquality axiomEquality cumulativity addLevel independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality independent_functionElimination approximateComputation unionElimination applyLambdaEquality equalitySymmetry equalityTransitivity dependent_pairFormation productElimination independent_isectElimination natural_numberEquality sqequalRule because_Cache applyEquality lambdaEquality isectElimination extract_by_obid hypothesisEquality dependent_functionElimination hypothesis lambdaFormation sqequalHypSubstitution rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution dependent_set_memberEquality productEquality

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m|  Surj(\mBbbN{}n;\mBbbN{}m;f)\}  ].
(inv(f)  \mmember{}  \{g:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}m;\mBbbN{}n;g)  \mwedge{}  (\mforall{}x:\mBbbN{}m.  ((f  (g  x))  =  x))\}  )

Date html generated: 2019_06_20-PM-01_17_35
Last ObjectModification: 2018_08_25-AM-08_20_11

Theory : int_2

Home Index